aboutsummaryrefslogtreecommitdiff
path: root/tactics/auto.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-07-03 18:54:06 +0200
committerMaxime Dénès2016-07-03 18:54:06 +0200
commite278d031a1d9a7bf3de463d3d415065299c99395 (patch)
treeddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /tactics/auto.ml
parentd7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff)
parent3ce70f21a18cc19e720e8ac54b93652527881942 (diff)
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
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 6c1f38d48b..962af4b5c5 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