diff options
Diffstat (limited to 'test-suite/bugs/closed/7779.v')
-rw-r--r-- | test-suite/bugs/closed/7779.v | 15 |
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 00000000..78936b59 --- /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. |