Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 12 insertions, 0 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a4d7251..cdeff601 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -986,6 +986,18 @@ let inNotation : notation_obj -> obj =
        classify_function = classify_notation}
 
 (**********************************************************************)
+
+let with_lib_stk_protection f x =
+  let fs = Lib.freeze () in
+  try let a = f x in Lib.unfreeze fs; a
+  with e -> Lib.unfreeze fs; raise e
+
+let with_syntax_protection f x =
+  with_lib_stk_protection
+    (with_grammar_rule_protection
+       (with_notation_protection f)) x
+
+(**********************************************************************)
 (* Recovering existing syntax                                         *)
 
 let contract_notation ntn =