From ac4ba8bbc899c3d3db1f1f5e0592ee419ed92994 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 24 Apr 2009 11:06:46 +0000
Subject: Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
 clause resulting in stray notations for e.g. variable named "le") and 12083
 (fixing bug in as clause of apply in) from trunk.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 6ffb36e411..ec3da0f8c5 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -410,7 +410,7 @@ let interp_recursive fixkind l boxed =
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs = 
-    States.with_heavy_rollback (fun () -> 
+    States.with_state_protection (fun () -> 
       List.iter (Command.declare_interning_data impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
-- 
cgit v1.2.3