Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).

We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.

1 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_12787.v b/test-suite/bugs/closed/bug_12787.v
new file mode 100644
index 0000000000..2566e1f261
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12787.v
@@ -0,0 +1,26 @@
+Inductive sigT3 {A: Type} {P: A -> Type} (Q: forall a: A, P a -> Type) :=
+  existT3: forall a: A, forall b: P a, Q a b -> sigT3 Q
+.
+
+Definition projT3_1 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) :=
+  let 'existT3 _ x0 _ _ := a in x0.
+
+Definition projT3_2 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) : P (projT3_1 a) :=
+  let 'existT3 _ x0 x1 _ := a in x1.
+
+
+
+Lemma projT3_3_eq' (A B: Type) (Q: B -> Type) (a b: sigT3 (fun (_: A) b => Q b)) (H: a = b) :
+  unit.
+Proof.
+  destruct a as [x0 x1 x2], b as [y0 y1 y2].
+  assert (H' := f_equal projT3_1 H).
+  cbn in H'.
+  subst x0.
+  assert (H' := f_equal (projT3_2 (P := fun _ => B)) H).
+  cbn in H'.
+  subst x1.
+
+  injection H as H'.
+  exact tt.
+Qed.