aboutsummaryrefslogtreecommitdiff
path: root/library/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.ml')
-rw-r--r--library/impargs.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 217169a610..56dca8e3f3 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -75,10 +75,10 @@ let with_implicits flags f x =
let rslt = f x in
implicit_args := oflags;
rslt
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = implicit_args := oflags in
- raise e
+ raise reraise
let set_maximality imps b =
(* Force maximal insertion on ending implicits (compatibility) *)