Fix SSR 'case B:b' with universe polymorphic equality

1 files changed, 10 insertions, 3 deletions

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index dbc9bb24c5..3a0868b7e4 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -383,15 +383,22 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in
         let gl, t = pfe_type_of gl c in
         let gl, eq = get_eq_type gl in
-        let gen_eq_tac, gl =
+        let gen_eq_tac, eq_ty, gl =
           let refl = EConstr.mkApp (eq, [|t; c; c|]) in
           let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in
           let new_concl = fire_subst gl new_concl in
           let erefl, gl = mkRefl t c gl in
           let erefl = fire_subst gl erefl in
-          apply_type new_concl [erefl], gl in
+          let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in
+          let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in
+          let gen_eq_tac s =
+            let open Evd in
+            let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in
+            apply_type new_concl [erefl] { s with sigma }
+          in
+          gen_eq_tac, eq_ty, gl in
         let rel = k + if c_is_head_p then 1 else 0 in
-        let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in
+        let src, gl = mkProt eq_ty EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in
         let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in
         let clr = if deps <> [] then clr else [] in
         concl, gen_eq_tac, clr, gl