diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 19:49:02 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-28 22:04:41 +0100 |
commit | 08da05299d32886bb516124fa497347b40249006 (patch) | |
tree | 14d186a8ae04c09ab6f1e13eb0e204a7b5867519 /test-suite | |
parent | 4b4e8b2b022c73bf0e73c28e60e2dc05fd0dbf8e (diff) |
In injection/inversion, consider all template-polymorphic types as injectable.
In particular singleton inductive types are considered injectable,
even in the absence of the option "Set Keep Proof Equalities".
This fixes #3125 (and #4560, #6273).
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/3125.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v new file mode 100644 index 000000000..797146174 --- /dev/null +++ b/test-suite/bugs/closed/3125.v @@ -0,0 +1,27 @@ +(* Not considering singleton template-polymorphic inductive types as + propositions for injection/inversion *) + +(* This is also #4560 and #6273 *) + +Inductive foo := foo_1. + +Goal forall (a b : foo), Some a = Some b -> a = b. +Proof. + intros a b H. + inversion H. + reflexivity. +Qed. + +(* Check that Prop is not concerned *) + +Inductive bar : Prop := bar_1. + +Goal + forall (a b : bar), + Some a = Some b -> + a = b. +Proof. + intros a b H. + inversion H. + Fail reflexivity. +Abort. |