Changeset 2781 for src


Ignore:
Timestamp:
Mar 6, 2013, 3:00:24 AM (7 years ago)
Author:
sacerdot
Message:

One more computational daemon closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2761 r2781  
    879879        let ppc ≝ lookup_labels (\fst newident_oldident) in
    880880         insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (renamed_symbols p))
    881      ? ?.
     881     (sigma (lookup_labels (final_label p))) ?.
    882882  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    883883    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     
    891891      [ #Hfold5 <Hfold5 % >Hfold1 %
    892892      | * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]]
    893   | cases daemon
    894893  | cases daemon
    895894  | * #sigma_pol_ok1 #_ #instr_list_ok %
Note: See TracChangeset for help on using the changeset viewer.