Changeset 2947

Timestamp:

Mar 24, 2013, 9:17:34 PM (8 years ago)

Author:

campbell

Message:

Init change in measurable to structured file.

File:

• src/RTLabs/MeasurableToStructured.ma (modified) (1 diff)

src/RTLabs/MeasurableToStructured.ma

@@ -82 +82 @@
 λp.
   let ge ≝ make_global p in
-  do m ← init_mem … (λx.[Init_space x]) p;
+  do m ← init_mem … (λx.x) p;
   let main ≝ prog_main ?? p in
   do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);