aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/pcoq.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index d1a6e0eda2..55558eaed0 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -685,9 +685,9 @@ let with_grammar_rule_protection f x =
let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = unfreeze fs in
- iraise reraise
+ Exninfo.iraise reraise
(** Registering grammar of generic arguments *)