Tweak version test in VSUpile

PrincetonUniversity · Oct 11, 2023 · 44d3ee2 · 44d3ee2
1 parent 848a90f
commit 44d3ee2
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/progs/VSUpile/verif_stdlib.v b/progs/VSUpile/verif_stdlib.v
@@ -6,11 +6,12 @@ Require Import spec_stdlib.
 
 Require VST.veric.version. From Coq Require Import String.
 Lemma version_test: False.
- assert (VST.veric.version.compcert_version = stdlib.Info.version \/
-         VST.veric.version.compcert_version = "3.13"%string /\
-	       stdlib.Info.version = "3.12"%string \/
-         VST.veric.version.compcert_version = "3.13"%string /\
-	       stdlib.Info.version = "3.11"%string)
+ assert ((VST.veric.version.compcert_version = "3.11"%string \/
+          VST.veric.version.compcert_version = "3.12"%string \/ 
+          VST.veric.version.compcert_version = "3.13"%string) /\
+         (stdlib.Info.version = "3.11"%string \/
+          stdlib.Info.version = "3.12"%string \/
+          stdlib.Info.version = "3.13"%string))
        by (compute; auto;
             match goal with |- ?G => fail 100 "Version mismatch; cannot prove" G end).
  assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by