5 files changed, 6 insertions, 10 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 007d139a33..f049963f1c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl =
   let cl' = Vars.subst_var id (pf_concl gl) in
   match pf_get_hyp gl id, mode with
   | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" ->
-     Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl')))
+     Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl')))
        [EConstr.of_constr (mkVar id)]) gl
   | NamedDecl.LocalDef (_, v, t), _ ->
      Proofview.V82.of_tactic
@@ -1193,13 +1193,13 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
     else let gl, ccl =  pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl
   else if to_ind && occ = None then
     let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in
-    let ucst = Evd.union_evar_universe_context ucst ucst' in
+    let ucst = UState.union ucst ucst' in
     if nv = 0 then anomaly "occur_existential but no evars" else
     let gl, pty = pfe_type_of gl p in
     false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl
   else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match")
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
+let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs)
 
 let genclrtac cl cs clr =
   let tclmyORELSE tac1 tac2 gl =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 7c16e1ba91..2b8f1d5409 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -414,6 +414,8 @@ val clr_of_wgen :
 
 val unfold : EConstr.t list -> unit Proofview.tactic
 
+val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac
+
 (* New code ****************************************************************)
 
 (* To call old code *)
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 33ebe26b6c..717657a247 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration
 
 (** The "case" and "elim" tactic *)
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
 (* TASSI: given the type of an elimination principle, it finds the higher order
  * argument (index), it computes it's arity and the arity of the eliminator and
  * checks if the eliminator is recursive or not *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 00c971237d..57635edac4 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -216,7 +216,7 @@ let same_proj sigma t1 t2 =
 let all_ok _ _ = true
 
 let fake_pmatcher_end () =
-  mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp)
+  mkProp, L2R, (Evd.empty, UState.empty, mkProp)
 
 let unfoldintac occ rdx t (kt,_) gl = 
   let fs sigma x = Reductionops.nf_evar sigma x in
@@ -372,8 +372,6 @@ let is_construct_ref sigma c r =
   EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r
 let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
 let rwcltac cl rdx dir sr gl =
   let n, r_n,_, ucst = pf_abs_evars gl sr in
   let r_n' = pf_abs_cterm gl n r_n in
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index cdf1c6f953..9cc4f5cece 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl =
   if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else
   errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical")
 
-let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs)
-
 let tclCLAUSES tac (gens, clseq) gl =
   if clseq = InGoal || clseq = InSeqGoal then tac gl else
   let clr_gens = pf_clauseids gl gens clseq in