Changeset 1618 for src/Clight/test

Timestamp:

Dec 14, 2011, 6:17:53 PM (10 years ago)

Author:

campbell

Message:

Minor updates due to recent changes.

Location:

src/Clight/test

Files:

• search.c.ma (modified) (2 diffs)
• sum.test.ma (modified) (2 diffs)

src/Clight/test/search.c.ma

@@ -215 +215 @@
 @refl
 qed.
-
+(*
 example csc: True.
 letin yyy ≝ (
@@ -228 +228 @@
 letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
 @⊥ normalize in xxx;
+*)

src/Clight/test/sum.test.ma

@@ -33 +33 @@
 @refl
 qed.
-
+(*
 include "RTLabs/RTLabsToRTL.ma".
 include alias "basics/lists/list.ma".
@@ -60 +60 @@
 [2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
 normalize in xxx
-
+*)