1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(* Not considering singleton template-polymorphic inductive types as
propositions for injection/inversion *)
(* This is also #4560 and #6273 *)
#[universes(template)]
#[warnings="-no-template-universe"]
Inductive foo := foo_1.
Add Keep Equalities foo.
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.
|
