3 files changed, 8 insertions, 9 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 513f5ca77b..d0c94e7903 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -670,7 +670,7 @@ let hResolve id c occ t =
       Pretyping.understand env sigma t_hole
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
-          let (e, info) = CErrors.push e in
+          let (e, info) = Exninfo.capture e in
           let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
           resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
   in
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 8344f9dae3..82c64a9857 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,7 +114,7 @@ END
 
 (** Eauto *)
 
-TACTIC EXTEND prolog
+TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
 | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
     { Eauto.prolog_tac (eval_uconstrs ist l) n }
 END
@@ -253,4 +253,3 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
           (match dbnames with None -> ["core"] | Some l -> l) entry;
  }
 END
-
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6e620b71db..1d7fe335d1 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) =
 let catch_error call_trace f x =
   try f x
   with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    catching_error call_trace iraise e
+    let e = Exninfo.capture e in
+    catching_error call_trace Exninfo.iraise e
 
 let wrap_error tac k =
   if is_traced () then Proofview.tclORELSE tac k else tac
@@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function
      try
         f ist env sigma c
      with reraise ->
-       let reraise = CErrors.push reraise in
+       let reraise = Exninfo.capture reraise in
        (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
-       iraise reraise
+       Exninfo.iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist env sigma c =
@@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c =
     try
       interp_may_eval interp_constr ist env sigma c
     with reraise ->
-      let reraise = CErrors.push reraise in
+      let reraise = Exninfo.capture reraise in
       (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term"));
-      iraise reraise
+      Exninfo.iraise reraise
   in
   begin
     (* spiwack: to avoid unnecessary modifications of tacinterp, as this