- Timestamp:
- Oct 17, 2011, 1:58:47 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/semantics.ma
r1385 r1386 88 88 qed. 89 89 90 definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝91 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params92 rtl_init_locals rtl_save_frame.93 94 90 (*CSC: XXXX, for external functions only*) 95 91 axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val). … … 117 113 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝ 118 114 λglobals. 119 mk_more_sem_params2 … rtl_more_sem_params 1115 mk_more_sem_params2 … rtl_more_sem_params 120 116 (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …) 121 (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …). 117 rtl_init_locals rtl_save_frame (rtl_pop_frame …) 118 rtl_fetch_external_args rtl_set_result (rtl_exec_extended …). 122 119 123 120 definition rtl_fullexec ≝
Note: See TracChangeset
for help on using the changeset viewer.