Ignore:
Timestamp:
Jun 3, 2011, 5:35:30 PM (9 years ago)
Author:
campbell
Message:

Refine "AST" types to include size/signedness information.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r797 r879  
    440440    #H1 #H2
    441441    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
    442     whd; inversion H2; #x #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     442    whd; inversion H2; #x #sz [ #sg ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
    443443    @refl
    444444| #v #f #env #k #m @refl
Note: See TracChangeset for help on using the changeset viewer.