Changeset 1634 for src/Clight/test

Timestamp:

Jan 4, 2012, 7:42:47 PM (9 years ago)

Author:

campbell

Message:

Update memory model examples syntax.

File:

• src/Clight/test/memorymodel.ma (modified) (5 diffs)

src/Clight/test/memorymodel.ma

@@ -29 +29 @@
   letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));
 
-  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
+  lapply (refl ? r); elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
   | #rr #_ @rr ] qed.
 
@@ -36 +36 @@
   letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));
 
-  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
+  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
   | #rr #_ @ rr ] qed.
   
@@ -48 +48 @@
        by the language). *)
 definition store4 := free store3 block.
-definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.
+definition store5 : mem. letin r ≝ (free store3 block); whd in r; @r qed.
 
 (* No ordering is imposed on deallocation (even though alloc and free are only used for
@@ -57 +57 @@
 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
-whd in r @r qed.
+whd in r; @r qed.
 
 (* Access to the "object representation" (as the C standard puts it) is not specified. *)
@@ -64 +64 @@
 definition storeIII : mem.
  letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
-  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
+  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
   | #rr #_ @rr ] qed.
 definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.