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

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r879 r882  
    195195| #ty #e #He whd in ⊢ (???%)
    196196    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
    197     @eval_Ederef [ 3: >Hv in He #He @He | *: skip ]
     197    >Hv in He #He
     198    @eval_Ederef [ 3: @He | *: skip ]
    198199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
    199200  cases ty // *#pty
     
    367368    cases ty cases v // #v' #sz try #sg
    368369    @bind_OK #evs #CHECK
    369     @(evl_match_cons ??????? (P_res_to_P CHECK)) //
     370    @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECK)) //
    370371  ]
    371372] qed.
Note: See TracChangeset for help on using the changeset viewer.