From c464965df350ab5007d2a1c0d6e625d119abf650 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jun 2018 14:44:33 +0200 Subject: 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 []. --- test-suite/bugs/closed/7779.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/bugs/closed/7779.v (limited to 'test-suite/bugs') 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. -- cgit v1.2.3