3 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index fa58a1c39a..0a781ea8a9 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
-    Tacmach.refine_no_check t gl
+    Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e92489e568..e25c93bf0a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm
 val mk_ast_closure_term :
   [ `None | `Parens | `DoubleParens | `At ] ->
   Constrexpr.constr_expr -> ast_closure_term
-val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal
+val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal
 Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term
 val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
 val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d09b81593e..1bd88ae3dd 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -398,7 +398,7 @@ let revtoptac n0 gl =
   let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
   let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
   let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
-  refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl
+  Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
 
 let equality_inj l b id c gl =
   let msg = ref "" in