diff options
| author | SimonBoulier <simon.boulier@ens-rennes.fr> | 2020-03-17 09:20:50 (GMT) |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2020-03-20 11:30:08 (GMT) |
| commit | debf64a9806e1cbe1bc26f18f1e3ce626224f8b3 (patch) | |
| tree | 72838f430ee2f72cc7a3992ce76d1f2f3492c8ef /test-suite | |
| parent | ec4a5f6059bd039e1d5bc0f746a89ddf92ccc967 (diff) | |
| download | coq-debf64a9806e1cbe1bc26f18f1e3ce626224f8b3.zip coq-debf64a9806e1cbe1bc26f18f1e3ce626224f8b3.tar.gz coq-debf64a9806e1cbe1bc26f18f1e3ce626224f8b3.tar.bz2 | |
Add test for PR11811 (disable a positivity check)
(cherry picked from commit b62a6df9907169f47a72ee78ebe088c68932dd93)
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_11811.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11811.v b/test-suite/bugs/closed/bug_11811.v new file mode 100644 index 0000000..a73494b --- /dev/null +++ b/test-suite/bugs/closed/bug_11811.v @@ -0,0 +1,13 @@ + +Unset Positivity Checking. + +Inductive foo : Type -> Type := +| bar : foo (foo unit) +| baz : foo nat. + +Definition toto : forall A, foo A -> {A = foo unit} + {A = nat}. +Proof. + intros A x. destruct x; intuition. +Defined. + +Check (eq_refl : toto _ baz = right eq_refl). |