Commit 9be882d3 authored by Léon Gondelman's avatar Léon Gondelman

move the test file into tests/

parent bff1360b
......@@ -13,7 +13,7 @@ theories/vcgen/dcexpr.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/test.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
# theories/heap_lang_vcgen/dval.v
# theories/heap_lang_vcgen/vcgen.v
......
......@@ -76,7 +76,8 @@ Section tests_vcg.
simpl. auto.
Qed.
Lemma test5 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
(*
Lemma test6 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
(∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
(∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗
l ↦C #1 -∗
......@@ -101,4 +102,5 @@ Section tests_vcg.
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#14)). eauto with iFrame.
Qed.
*)
End tests_vcg.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment