Merge PR #8866: Check universe instances in Typing

1 files changed, 10 insertions, 7 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25f9bc5576..5cead11a5c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4097,12 +4097,15 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
-  let evd, elimc =
-    if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
+  let env = Tacmach.New.pf_env gl in
+  let sigma = Tacmach.New.project gl in
+  let sigma, elimc =
+    if isrec && not (is_nonrec mind)
+    then
+      let gr = lookup_eliminator mind s in
+      Evd.fresh_global env sigma gr
     else
-      let env = Tacmach.New.pf_env gl in
-      let sigma = Tacmach.New.project gl in
-      let u = EInstance.kind (Tacmach.New.project gl) u in
+      let u = EInstance.kind sigma u in
       if dep then
         let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
@@ -4112,8 +4115,8 @@ let guess_elim isrec dep s hyp0 gl =
         let ind = EConstr.of_constr ind in
         (sigma, ind)
   in
-  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
-    evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+  let elimt = Typing.unsafe_type_of env sigma elimc in
+    sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in