From 85dd53ed83f229044f2b19a9ef46387ff981aa57 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 23 Apr 2013 18:16:16 +0000
Subject: Indfun : use States.with_state_protection instead of freeze/unfreeze

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16447 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun.ml | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 609e2916da..fcd1c5360e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -154,19 +154,12 @@ let build_newrecursive
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
-    let fs = States.freeze() in
-    let def =
-      try
-	List.map
-	  (fun (_,bl,_,def)  ->
-             let def = abstract_glob_constr def bl in
-             interp_casted_constr_with_implicits
-	       sigma rec_sign rec_impls def
-	  )
-          lnameargsardef
-	with reraise ->
-	States.unfreeze fs; raise reraise in
-    States.unfreeze fs; def
+    let f (_,bl,_,def) =
+      let def = abstract_glob_constr def bl in
+      interp_casted_constr_with_implicits
+        sigma rec_sign rec_impls def
+    in
+    States.with_state_protection (List.map f) lnameargsardef
   in
   recdef,rec_impls
 
-- 
cgit v1.2.3