summaryrefslogtreecommitdiff
path: root/test-suite/success/intros.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/intros.v')
-rw-r--r--test-suite/success/intros.v24
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index a329894a..d37ad9f5 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -127,4 +127,28 @@ induction 1 as (n,H,IH).
exact Logic.I.
Qed.
+(* Make "intro"/"intros" progress on existential variables *)
+Module Evar.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intro x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Goal exists (A:Prop), A.
+eexists.
+unshelve (intros x).
+- exact nat.
+- exact (x=x).
+- auto.
+Qed.
+
+Definition d := ltac:(intro x; exact (x*x)).
+
+Definition d' : nat -> _ := ltac:(intros;exact 0).
+
+End Evar.