Changeset 2158


Ignore:
Timestamp:
Jul 6, 2012, 11:41:40 AM (5 years ago)
Author:
sacerdot
Message:

One less daemon.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2157 r2158  
    850850qed.
    851851
    852 
    853 
    854852definition assembly:
    855853    ∀p: pseudo_assembly_program.
     
    958956    lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
    959957    cut (pc_delta < 2^16)
    960     [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq
     958    [ >EQpc_delta
     959      @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2)
     960      @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok
    961961    cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
    962962    [ whd in match instruction_size; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.