Changeset 2806 for src/ERTLptr


Ignore:
Timestamp:
Mar 7, 2013, 2:51:40 PM (8 years ago)
Author:
tranquil
Message:

new b_graph_translate obligations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2774 r2806  
    435435    (* init_stack_size ≝ *) stack_sz
    436436    (* added_prologue ≝ *) [ ]
     437    (* new_regs ≝ *) [ ]
    437438    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
    438439    (* f_fin ≝ *) (translate_fin_step globals)
    439     ???).
     440    ????).
    440441@hide_prf
    441 [ #l #c % ]
     442[
     443| #l #c % ]
    442444cases daemon (* TODO *)
    443445qed.
Note: See TracChangeset for help on using the changeset viewer.