aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6c1f38d48..962af4b5c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,7 @@
*)
open Pp
open Util
-open Errors
+open CErrors
open Names
open Vars
open Termops
@@ -222,7 +222,7 @@ let tclLOG (dbg,depth,trace) pp tac =
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
iraise reraise
end
@@ -234,7 +234,7 @@ let tclLOG (dbg,depth,trace) pp tac =
trace := (depth, Some pp) :: !trace;
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
trace := (depth, None) :: !trace;
iraise reraise
end