Changeset 1510 for src/common


Ignore:
Timestamp:
Nov 16, 2011, 4:38:41 PM (8 years ago)
Author:
sacerdot
Message:

All files ported to new dependent inversion.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Smallstep.ma

    r891 r1510  
    132132  plus tr ge s1 t s3.
    133133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
    134 [ #s2' #e2 #e3 #e4 destruct; @plus_one //;
    135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5
     134[ #s2' #e2 #e3 #e4 #e5s destruct; @plus_one //;
     135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 #e6
    136136    >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1)
    137137    [ 2: @(star_right … H2 Hstep) //;
     
    140140    ]
    141141]
    142 qed. 
     142qed.
    143143(*
    144144Lemma plus_left':
  • src/common/Values.ma

    r1369 r1510  
    10981098  ∀chunk,v1,v2.
    10991099  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1100 #chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
    1101 [ 8: #r ] whd in ⊢ (?%?); //; 
     1100#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
     1101[ 8: #r ] whd in ⊢ (?%?); //;
    11021102qed.
    11031103
Note: See TracChangeset for help on using the changeset viewer.