Ignore:
Timestamp:
Jun 6, 2011, 11:07:24 PM (9 years ago)
Author:
sacerdot
Message:

Minor changes because of the new, weaker (but much faster) delift.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r885 r889  
    762762     @eq_instruction_refl
    763763   | cases arg -i arg;
     764(* 
     76516,17,18,19,20,28,19
     766*)
    764767     [1,2,3: #arg1 #arg2
    765768       @(list_addressing_mode_tags_elim_prop … arg1) whd try %
     
    833836       >half_add_SO
    834837       >lookup_insert_hit
    835        >lookup_insert_miss try @not_eqvb_SS
     838       >lookup_insert_miss //
    836839       >lookup_insert_hit
    837840       normalize
Note: See TracChangeset for help on using the changeset viewer.