4 files changed, 4 insertions, 8 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f3c758e5c..f2f236f448 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
 
 (** Basic tactics *)
 
-let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl ->
+let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   match EConstr.kind (Proofview.Goal.sigma gl) concl with
   | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index e367cd32d6..f67cf20e49 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration
 (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
 (** Defined identifier *)
 
-
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
 
 let ssrposetac (id, (_, t)) gl =
   let ist, t =
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 8b9c94f2db..a7aae5bd31 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
 END
 
 let vmexacttac pf =
-  Goal.nf_enter begin fun gl ->
+  Goal.enter begin fun gl ->
   exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
   end
 
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 83581f3416..f12f9fac0f 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
 open Constr
 open Termops
 open Tacmach
-open Locusops
 
 open Ssrast
 open Ssrcommon
@@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq =
 
 let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
 
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
 
 let hidetacs clseq idhide cl0 =
   if not (hidden_clseq clseq) then  [] else