Changeset 882 for src/Clight


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

Fix up fragile proofs for current version of matita.

Location:
src/Clight
Files:
3 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.
  • src/Clight/TypeComparison.ma

    r880 r882  
    1313definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
    1414#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
    15 [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
     15[ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
    1616
    1717let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
  • src/Clight/toCminor.ma

    r881 r882  
    416416      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    417417      [ ASTptr r ⇒ λe1'.
    418           match access_mode ty return λx.access_mode ty = x → ? with
     418          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    419419          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    420420          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
Note: See TracChangeset for help on using the changeset viewer.