Vernacexpr is now a mli-only file, locality stuff now in locality.ml

 Adds a directory ./intf for pure interfaces.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 8 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fb9439d73e..2700b2b7d5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -613,6 +613,6 @@ END
 VERNAC COMMAND EXTEND HintCut
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
   let entry = HintsCutEntry p in
-    Auto.add_hints (Vernacexpr.use_section_locality ()) 
+    Auto.add_hints (Locality.use_section_locality ())
       (match dbnames with None -> ["core"] | Some l -> l) entry ]
 END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 458c5bec66..88170d6dd7 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1477,7 +1477,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 (dummy_loc,None,fields)))
-    ~global:(not (Vernacexpr.use_section_locality ())) ~generalize:false None
+    ~global:(not (Locality.use_section_locality ())) ~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"
@@ -1496,7 +1496,7 @@ let declare_instance_trans global binders a aeq n lemma =
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let global = not (Vernacexpr.use_section_locality ()) in
+  let global = not (Locality.use_section_locality ()) in
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
   in ignore(anew_instance global binders instance []);
   match (refl,symm,trans) with
@@ -1754,16 +1754,16 @@ let add_morphism glob binders m s n =
 
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ add_setoid (not (Vernacexpr.use_section_locality ())) [] a aeq t n ]
+     [ add_setoid (not (Locality.use_section_locality ())) [] a aeq t n ]
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [	add_setoid (not (Vernacexpr.use_section_locality ())) binders a aeq t n ]
+     [	add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ]
+      [ add_morphism_infer (not (Locality.use_section_locality ())) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ]
+      [ add_morphism (not (Locality.use_section_locality ())) [] m s n ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
 	"with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ]
+      [ add_morphism (not (Locality.use_section_locality ())) binders m s n ]
 END
 
 (** Bind to "rewrite" too *)