Changeset 1080


Ignore:
Timestamp:
Jul 19, 2011, 5:28:38 PM (8 years ago)
Author:
mulligan
Message:

more added

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r784 r1080  
    3939    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    4040    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    41     let rtl_if_sig' ≝ rtl_if_sig def in
    4241    let rtl_if_result' ≝ rtl_if_result def in
    4342    let rtl_if_params' ≝ rtl_if_params def in
     
    4847    let rtl_if_exit' ≝ rtl_if_exit def in
    4948      mk_rtl_internal_function
    50         rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
     49        rtl_if_luniverse' rtl_if_runiverse'
    5150        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    52         rtl_if_graph' rtl_if_entry' rtl_if_exit'.
     51        rtl_if_graph' ? ?.
     52  [1: normalize nodelta;
    5353
    5454definition simplify_funct ≝
  • src/common/Graphs.ma

    r1077 r1080  
    2626  ∀to_insert: label.
    2727    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
     28
     29axiom graph_num_nodes:
     30  ∀A: Type[0].
     31  ∀g: graph A.
     32    nat.
Note: See TracChangeset for help on using the changeset viewer.