From a554519874c15d0a790082e5f15f3dc2419c6c38 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 19 Nov 2017 04:47:15 +0100
Subject: [lib] Minor pending cleanup to consolidate helper function.

While we are at it we refactor a few special cases of the helper.
---
 interp/constrextern.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e1cf8f196d..0ce672cc83 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -185,18 +185,8 @@ let with_universes f = Flags.with_option print_universes f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 let without_symbols f = Flags.with_option print_no_symbol f
 
-(* XXX: Where to put this in the library? Util maybe? *)
-let protect_ref r nf f x =
-  let old_ref = !r in
-  r := nf !r;
-  try let res = f x in r := old_ref; res
-  with reraise ->
-    let reraise = Backtrace.add_backtrace reraise in
-    r := old_ref;
-    Exninfo.iraise reraise
-
 let without_specific_symbols l =
-  protect_ref inactive_notations_table
+  Flags.with_modified_ref inactive_notations_table
     (fun tbl -> IRuleSet.(union (of_list l) tbl))
 
 (**********************************************************************)
-- 
cgit v1.2.3