Changeset 1522 for src/ASM/Status.ma


Ignore:
Timestamp:
Nov 21, 2011, 3:49:04 PM (8 years ago)
Author:
mulligan
Message:

changes to preamble and lin to asm pass, resolved conflict in interpret

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1521 r1522  
    11541154 #id #id' #i #prefix elim prefix
    11551155  [ whd in ⊢ (?% → ?);
    1156     change in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?); with (eq_identifier ? id' id);
     1156    change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11571157    @eq_identifier_elim normalize nodelta; /2/
    11581158  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    11591159    cases he; normalize nodelta
    11601160     [ #H @ (IH H)
    1161      | #x whd in ⊢ (? → ?(??%)); change in match (instruction_matches_identifier ??); with (eq_identifier ? x id)
     1161     | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
    11621162       @eq_identifier_elim #E normalize nodelta
    11631163       [ destruct @eq_identifier_elim normalize nodelta;
     
    11721172    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    11731173 #id #id' #i #prefix elim prefix
    1174  [ whd in ⊢ (?% → ?); change in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?); with (eq_identifier ???)
     1174 [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
    11751175   @eq_identifier_elim #E
    11761176  [ normalize //
     
    11851185       | #H >(does_not_occur_Some)
    11861186         [ #H2 whd in match (does_not_occur ??);
    1187            change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1187           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    11881188           >Heq >eq_identifier_refl normalize nodelta
    11891189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
    1190            change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1190           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    11911191           >eq_identifier_refl
    11921192           normalize nodelta @H2 
     
    11981198       #Hor @orb_elim
    11991199       [ <Heq2 in Hor; #Hor normalize in Hor;
    1200          whd in match (does_not_occur ??); change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1200         whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    12011201         >eq_identifier_false // normalize nodelta
    12021202         cases (does_not_occur id' tl) in Hor; normalize nodelta //
    12031203       | normalize nodelta whd in match (occurs_exactly_once ??);
    1204          change in match (instruction_matches_identifier ??); with (eq_identifier ???)
     1204         change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    12051205         >eq_identifier_false //
    12061206       ]
Note: See TracChangeset for help on using the changeset viewer.