aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-12 14:44:33 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-12 14:44:33 +0200
commitc464965df350ab5007d2a1c0d6e625d119abf650 (patch)
treed6651eb90ab000743ad79863706aba9e3c1a96f6 /test-suite
parentab4bce38a7c0d08d1ebff70c4115b7c1d8e8be88 (diff)
Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").
This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using [].
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/7779.v15
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7779.v b/test-suite/bugs/closed/7779.v
new file mode 100644
index 000000000..78936b595
--- /dev/null
+++ b/test-suite/bugs/closed/7779.v
@@ -0,0 +1,15 @@
+(* Checking that the "in" clause takes the "eqn" clause into account *)
+
+Definition test (x: nat): {y: nat | False }. Admitted.
+
+Parameter x: nat.
+Parameter z: nat.
+
+Goal
+ proj1_sig (test x) = z ->
+ False.
+Proof.
+ intro H.
+ destruct (test x) eqn:Heqs in H.
+ change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
+Abort.