- Timestamp:
- Sep 21, 2011, 11:57:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/semantics.ma
r1141 r1233 264 264 [ nil ⇒ Some ? (smerge2 v) 265 265 | _ ⇒ None ? ]]. 266 266 (* 267 267 definition RTL_exec : execstep io_out io_in ≝ 268 268 mk_execstep … ? is_final mem_of_state eval_statement. 269 269 *) 270 270 (* CSC: XXX the program type does not fit with the globalenv and init_mem 271 271 definition make_initial_state : rtl_program → res (genv × state) ≝
Note: See TracChangeset
for help on using the changeset viewer.