diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/proof_using.v | 3 | ||||
| -rw-r--r-- | test-suite/success/refine.v | 2 | ||||
| -rw-r--r-- | test-suite/success/unshelve.v | 11 |
3 files changed, 14 insertions, 2 deletions
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index c83f45e2a4..adaa05ad06 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -178,6 +178,7 @@ End Let. Check (test_let 3). +(* Disabled Section Clear. Variable a: nat. @@ -192,6 +193,6 @@ trivial. Qed. End Clear. - +*) diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 1e667884b8..352abb2af5 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,7 +62,7 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -2:reflexivity. +reflexivity. Abort. (* Submitted by Jacek Chrzaszcz (bug #1102) *) diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v new file mode 100644 index 0000000000..672222bdd6 --- /dev/null +++ b/test-suite/success/unshelve.v @@ -0,0 +1,11 @@ +Axiom F : forall (b : bool), b = true -> + forall (i : unit), i = i -> True. + +Goal True. +Proof. +unshelve (refine (F _ _ _ _)). ++ exact true. ++ exact tt. ++ exact (@eq_refl bool true). ++ exact (@eq_refl unit tt). +Qed. |