diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/6878.v | 8 | ||||
-rw-r--r-- | test-suite/output/Load.out | 6 | ||||
-rw-r--r-- | test-suite/output/Load.v | 7 | ||||
-rw-r--r-- | test-suite/output/load/Load_noproof.v | 1 | ||||
-rw-r--r-- | test-suite/output/load/Load_openproof.v | 1 | ||||
-rw-r--r-- | test-suite/output/load/Load_proof.v | 2 | ||||
-rw-r--r-- | test-suite/success/rewrite.v | 17 |
7 files changed, 41 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 000000000..70f1b3127 --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out new file mode 100644 index 000000000..0904d5540 --- /dev/null +++ b/test-suite/output/Load.out @@ -0,0 +1,6 @@ +f = 2 + : nat +u = I + : True +The command has indeed failed with message: +Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v new file mode 100644 index 000000000..967507415 --- /dev/null +++ b/test-suite/output/Load.v @@ -0,0 +1,7 @@ +Load "output/load/Load_noproof.v". +Print f. + +Load "output/load/Load_proof.v". +Print u. + +Fail Load "output/load/Load_openproof.v". diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v new file mode 100644 index 000000000..aaf1ffe26 --- /dev/null +++ b/test-suite/output/load/Load_noproof.v @@ -0,0 +1 @@ +Definition f := 2. diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v new file mode 100644 index 000000000..204d4ecbf --- /dev/null +++ b/test-suite/output/load/Load_openproof.v @@ -0,0 +1 @@ +Lemma k : True. diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v new file mode 100644 index 000000000..e47f66a19 --- /dev/null +++ b/test-suite/output/load/Load_proof.v @@ -0,0 +1,2 @@ +Lemma u : True. +Proof. exact I. Qed. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 62249666b..448d0082d 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -151,10 +151,25 @@ Abort. (* Check that rewriting within evars still work (was broken in 8.5beta1) *) - Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y. intros; eexists; eexists. rewrite H. Undo. subst. Abort. + +(* Check that iterated rewriting does not rewrite in the side conditions *) +(* Example from Sigurd Schneider, extracted from contrib containers *) + +Lemma EQ + : forall (e e' : nat), True -> e = e'. +Admitted. + +Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1. +Proof. + rewrite <- (EQ v1 v2) in *. + exact v'. + (* There should be only two side conditions *) + exact I. + exact I. +Qed. |