Merge PR coq#19207: Fix remember with sort polymorphic equality and…

… values

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

tactics/tactics.ml

@@ -2699,10 +2699,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
           let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
           let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
           let sigma, eq = Typing.checked_applist env sigma eq [t] in
+          let sigma, refl = Typing.checked_applist env sigma refl [t] in
           let eq = applist (eq, args) in
-          let refl = applist (refl, [t;mkVar id]) in
+          let refl = applist (refl, [mkVar id]) in
+          let r = Retyping.relevance_of_term env sigma refl in
           let term = mkNamedLetIn sigma (make_annot id rel) c t
-              (mkLetIn (make_annot (Name heq) ERelevance.relevant, refl, eq, ccl)) in
+              (mkLetIn (make_annot (Name heq) r, refl, eq, ccl)) in
           let ans = term,
             Tacticals.tclTHENLIST
               [

test-suite/bugs/bug_19203.v

@@ -0,0 +1,40 @@
+Set Universe Polymorphism.
+
+Inductive bool@{q| |} : Type@{q|Set} := | true : bool | false : bool.
+
+Definition nand@{q| |} (a b : bool@{q|}) : bool@{q|} :=
+  match a , b with
+  | true , true => false
+  | _ , _ => true
+  end.
+
+Inductive seq@{q|u|} {A : Type@{q|u}} (a : A) : A -> Type@{q|u} := | srefl : seq a a.
+Arguments srefl {_ _}.
+
+Definition seq_elim@{q|u v|} :=
+  fun (A : Type@{q|u}) (x : A) (P : A -> Type@{q|v}) (f : P x) (a : A) (e : seq x a) =>
+  match e in (seq _ a0) return (P a0) with
+  | srefl => f
+  end.
+
+Register seq as core.eq.type.
+Register srefl as core.eq.refl.
+Register seq_elim as core.eq.rect.
+
+Lemma foo@{q| |} (f : bool@{q|} -> bool@{q|}) (x : bool@{q|}) : seq (f true) (f true).
+Proof.
+  remember (f true) as b eqn : ftrue.
+  reflexivity.
+Qed.
+
+Lemma f3_eq_f@{q| |} (f : bool@{q|} -> bool@{q|}) (x : bool@{q|}) : seq (f (f (f x))) (f x).
+Proof.
+  remember (f true) as b eqn : ftrue.
+
+  remember (f false) as c eqn : ffalse.
+  Validate Proof.
+
+  destruct x,b,c.
+  all:repeat rewrite <-?ftrue, <-?ffalse.
+  all: reflexivity.
+Qed.