From 6a05c7e546a9dd2065f35b788b35e7a85866dfc8 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 15 Apr 2013 13:33:32 +0000
Subject: anew_instance should not consume the locality twice

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16397 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index dc59005f68..19a2f390b5 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1587,7 +1587,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
   new_instance binders instance (Some (CRecord (Loc.ghost,None,fields)))
-    ~global:(not (Locality.use_section_locality ())) ~generalize:false None
+    ~global ~generalize:false None
 
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-- 
cgit v1.2.3