diff options
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3125.v | 27 |
2 files changed, 28 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c36ad980ef..0d6263246e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -739,7 +739,7 @@ let keep_proof_equalities = function let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in - let s = get_sort_family_of env sigma ty1 in + let s = get_sort_family_of ~truncation_style:true env sigma ty1 in if Sorts.List.mem s sorts then [(List.rev posn,t1,t2)] else [] in diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v new file mode 100644 index 0000000000..797146174d --- /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. |