1 files changed, 12 insertions, 13 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 6f8e668e4e..b0ea75ac60 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -302,7 +302,8 @@ let tclONCE = Proof.once
 
 exception MoreThanOneSuccess
 let _ = CErrors.register_handler begin function
-  | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
+  | MoreThanOneSuccess ->
+    Pp.str "This tactic has more than one success."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -347,8 +348,7 @@ exception NoSuchGoals of int
 
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    CErrors.user_err
-      (str "No such " ++ str (String.plural n "goal") ++ str ".")
+    str "No such " ++ str (String.plural n "goal") ++ str "."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
 exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
   | SizeMismatch (i,j) ->
-      let open Pp in
-      let errmsg =
-        str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
-      in
-      CErrors.user_err  errmsg
+    let open Pp in
+    str"Incorrect number of goals" ++ spc() ++
+    str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
   | _ -> raise CErrors.Unhandled
 end
 
@@ -910,7 +907,8 @@ let tclPROGRESS t =
     tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
 
 let _ = CErrors.register_handler begin function
-  | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Logic_monad.Tac_Timeout ->
+    Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
   | _ -> raise CErrors.Unhandled
 end
 
@@ -1039,9 +1037,9 @@ let (>>=) = tclBIND
 
 (** {6 Goal-dependent tactics} *)
 
-let goal_env evars gl =
+let goal_env env evars gl =
   let evi = Evd.find evars gl in
-  Evd.evar_filtered_env evi
+  Evd.evar_filtered_env env evi
 
 let goal_nf_evar sigma gl =
   let evi = Evd.find sigma gl in
@@ -1256,9 +1254,10 @@ module V82 = struct
 
   let of_tactic t gls =
     try
+      let env = Global.env () in
       let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
       let name, poly = Names.Id.of_string "legacy_pe", false in
-      let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
+      let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
     with Logic_monad.TacticFailure e as src ->
       let (_, info) = CErrors.push src in