From a3cee159e8b119bb21dad5c1bfb4173be21bbbfe Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Tue, 4 Jun 2019 14:09:27 +0200
Subject: Fix SSR 'case B:b' with universe polymorphic equality

---
 plugins/ssr/ssrelim.ml         | 13 ++++++++++---
 test-suite/ssr/case_polyuniv.v | 12 ++++++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/ssr/case_polyuniv.v

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
diff --git a/test-suite/ssr/case_polyuniv.v b/test-suite/ssr/case_polyuniv.v
new file mode 100644
index 0000000000..8774e191c1
--- /dev/null
+++ b/test-suite/ssr/case_polyuniv.v
@@ -0,0 +1,12 @@
+Require Import ssreflect.
+
+Set Universe Polymorphism.
+
+Cumulative Variant paths {A} (x:A) : A -> Type
+  := idpath : paths x x.
+
+Register paths as core.eq.type.
+Register idpath as core.eq.refl.
+
+Lemma case_test (b:bool) : paths b b.
+Proof. case B:b; reflexivity. Qed.
-- 
cgit v1.2.3