 Timestamp:
 Jul 19, 2011, 5:28:38 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r784 r1080 39 39 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 40 40 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 41 let rtl_if_sig' ≝ rtl_if_sig def in42 41 let rtl_if_result' ≝ rtl_if_result def in 43 42 let rtl_if_params' ≝ rtl_if_params def in … … 48 47 let rtl_if_exit' ≝ rtl_if_exit def in 49 48 mk_rtl_internal_function 50 rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'49 rtl_if_luniverse' rtl_if_runiverse' 51 50 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; 53 53 54 54 definition simplify_funct ≝ 
src/common/Graphs.ma
r1077 r1080 26 26 ∀to_insert: label. 27 27 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. 28 29 axiom graph_num_nodes: 30 ∀A: Type[0]. 31 ∀g: graph A. 32 nat.
Note: See TracChangeset
for help on using the changeset viewer.