summaryrefslogtreecommitdiff
path: root/library/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.ml')
-rw-r--r--library/impargs.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index c79edb99..930b8f09 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -74,9 +74,9 @@ let with_implicits flags f x =
let rslt = f x in
implicit_args := oflags;
rslt
- with e -> begin
+ with reraise -> begin
implicit_args := oflags;
- raise e
+ raise reraise
end
let set_maximality imps b =