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

25 files changed, 235 insertions, 178 deletions

diff --git a/CREDITS b/CREDITS
index 35057ea8f..c654db2ee 100644
--- a/CREDITS
+++ b/CREDITS
@@ -12,7 +12,7 @@ The "Coq proof assistant" was jointly developed by
 
 All files of the "Coq proof assistant" in directories or sub-directories of
 
-  config dev ide interp kernel lib library parsing pretyping proofs
+  config dev ide interp intf kernel lib library parsing pretyping proofs
   scripts states tactics test-suite theories tools toplevel
 
 are distributed under the terms of the GNU Lesser General Public License 
diff --git a/Makefile.common b/Makefile.common
index 22b06a40e..d5b152432 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -72,7 +72,7 @@ SRCDIRS:=\
   config 	tools 		tools/coqdoc 	scripts		lib \
   kernel	kernel/byterun	library 	proofs 		tactics \
   pretyping	interp		toplevel/utils	toplevel 	parsing 	\
-  ide/utils	ide		\
+  intf          ide/utils	ide		\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring \
     setoid_ring xml 		extraction 	fourier \
@@ -345,7 +345,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 
 OCAMLDOCDIR=dev/ocamldoc
 
-DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \
+DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
 	./pretyping/*.mli ./interp/*.mli \
 	./parsing/*.mli ./proofs/*.mli \
 	./tactics/*.mli ./toplevel/*.mli)
diff --git a/_tags b/_tags
index cf8319bd9..08dc9f1af 100644
--- a/_tags
+++ b/_tags
@@ -64,6 +64,7 @@
 "ide": include
 "ide/utils": include
 "interp": include
+"intf": include
 "kernel": include
 "kernel/byterun": include
 "lib": include
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 743205888..5358673ff 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -13,7 +13,7 @@ exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
 	-I $COQTOP \
 	-I $COQTOP/config \
-	-I $COQTOP/lib -I $COQTOP/kernel \
+	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
diff --git a/dev/printers.mllib b/dev/printers.mllib
index f93d01daf..c1a95cdb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -137,6 +137,6 @@ Tactic_printer
 Egrammar
 Himsg
 Cerrors
-Vernacexpr
+Locality
 Vernacinterp
 Top_printers
diff --git a/toplevel/vernacexpr.ml b/intf/vernacexpr.mli
index 95384c1c9..238400806 100644
--- a/toplevel/vernacexpr.ml
+++ b/intf/vernacexpr.mli
@@ -6,25 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
-open Errors
 open Pp
-open Util
 open Names
 open Tacexpr
-open Extend
 open Genarg
 open Topconstr
 open Decl_kinds
-open Ppextend
-open Declaremods
-
-(* Toplevel control exceptions *)
-exception Drop
-exception Quit
-
 open Libnames
-open Nametab
+
+(** Vernac expressions, produced by the parser *)
 
 type lident = identifier located
 type lname = name located
@@ -179,7 +169,7 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-type module_ast_inl = module_ast annotated
+type module_ast_inl = module_ast Declaremods.annotated
 type module_binder = bool option * lident list * module_ast_inl
 
 type grammar_tactic_prod_item_expr =
@@ -187,10 +177,10 @@ type grammar_tactic_prod_item_expr =
   | TacNonTerm of loc * string * (Names.identifier * string) option
 
 type syntax_modifier =
-  | SetItemLevel of string list * production_level
+  | SetItemLevel of string list * Extend.production_level
   | SetLevel of int
-  | SetAssoc of gram_assoc
-  | SetEntryType of string * simple_constr_prod_entry_key
+  | SetAssoc of Compat.gram_assoc
+  | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing
   | SetFormat of string located
 
@@ -276,8 +266,8 @@ type vernac_expr =
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
       module_binder list * module_ast_inl
-  | VernacDefineModule of bool option * lident *
-      module_binder list * module_ast_inl module_signature * module_ast_inl list
+  | VernacDefineModule of bool option * lident * module_binder list *
+      module_ast_inl Declaremods.module_signature * module_ast_inl list
   | VernacDeclareModuleType of lident *
       module_binder list * module_ast_inl list * module_ast_inl list
   | VernacInclude of module_ast_inl list
@@ -315,7 +305,7 @@ type vernac_expr =
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list list
-  | VernacArguments of locality_flag * reference or_by_notation * 
+  | VernacArguments of locality_flag * reference or_by_notation *
       ((name * bool * (loc * string) option * bool * bool) list) list *
       int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
@@ -365,133 +355,3 @@ type vernac_expr =
   | VernacExtend of string * raw_generic_argument list
 
 and located_vernac_expr = loc * vernac_expr
-
-
-(** Categories of [vernac_expr] *)
-
-let rec strip_vernac = function
-  | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c
-  | c -> c (* TODO: what about VernacList ? *)
-
-let rec is_navigation_vernac = function
-  | VernacResetInitial
-  | VernacResetName _
-  | VernacBacktrack _
-  | VernacBackTo _
-  | VernacBack _ -> true
-  | c -> is_deep_navigation_vernac c
-
-and is_deep_navigation_vernac = function
-  | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
-  | _ -> false
-
-(* Locating errors raised just after the dot is parsed but before the
-   interpretation phase *)
-
-let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)
-
-(**********************************************************************)
-(* Managing locality *)
-
-let locality_flag = ref None
-
-let local_of_bool = function true -> Local | false -> Global
-
-let check_locality () =
-  match !locality_flag with
-  | Some (loc,true) -> 
-      syntax_checking_error loc
-	"This command does not support the \"Local\" prefix.";
-  | Some (loc,false) -> 
-      syntax_checking_error loc
-	"This command does not support the \"Global\" prefix."
-  | None -> ()
-
-(** Extracting the locality flag *)
-
-(* Commands which supported an inlined Local flag *)
-
-let enforce_locality_full local =
-  let local =
-    match !locality_flag with
-    | Some (_,false) when local ->
-	error "Cannot be simultaneously Local and Global."
-    | Some (_,true) when local ->
-	error "Use only prefix \"Local\"."
-    | None ->
-	if local then begin
-	  Flags.if_warn
-	   Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
-	  Some true
-	end else
-	None
-    | Some (_,b) -> Some b in
-  locality_flag := None;
-  local
-
-(* Commands which did not supported an inlined Local flag (synonym of
-   [enforce_locality_full false]) *)
-
-let use_locality_full () =
-  let r = Option.map snd !locality_flag in
-  locality_flag := None;
-   r
-
-(** Positioning locality for commands supporting discharging and export
-     outside of modules *)
-
-(* For commands whose default is to discharge and export:
-   Global is the default and is neutral;
-   Local in a section deactivates discharge, 
-   Local not in a section deactivates export *)
-
-let make_locality = function Some true -> true | _ -> false
-
-let use_locality () = make_locality (use_locality_full ())
-
-let use_locality_exp () = local_of_bool (use_locality ())
-
-let enforce_locality local = make_locality (enforce_locality_full local)
-
-let enforce_locality_exp local = local_of_bool (enforce_locality local)
-
-(* For commands whose default is not to discharge and not to export:
-   Global forces discharge and export;
-   Local is the default and is neutral *)
-
-let use_non_locality () =
-  match use_locality_full () with Some false -> false | _ -> true
-
-(* For commands whose default is to not discharge but to export:
-   Global in sections forces discharge, Global not in section is the default;
-   Local in sections is the default, Local not in section forces non-export *)
-
-let make_section_locality =
-  function Some b -> b | None -> Lib.sections_are_opened ()
-
-let use_section_locality () =
-  make_section_locality (use_locality_full ())
-
-let enforce_section_locality local =
-  make_section_locality (enforce_locality_full local)
-
-(** Positioning locality for commands supporting export but not discharge *)
-
-(* For commands whose default is to export (if not in section):
-   Global in sections is forbidden, Global not in section is neutral;
-   Local in sections is the default, Local not in section forces non-export *)
-
-let make_module_locality = function
-  | Some false ->
-      if Lib.sections_are_opened () then
-	error "This command does not support the Global option in sections.";
-      false
-  | Some true -> true
-  | None -> false
-
-let use_module_locality () =
-  make_module_locality (use_locality_full ())
-
-let enforce_module_locality local =
-  make_module_locality (enforce_locality_full local)
diff --git a/lib/errors.ml b/lib/errors.ml
index 1060a8efd..026198a98 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -35,6 +35,8 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 exception Error_in_file of string * (bool * string * loc) * exn
 
 exception Timeout
+exception Drop
+exception Quit
 
 let handle_stack = ref []
 
diff --git a/lib/errors.mli b/lib/errors.mli
index a863c5e30..d04ebb3fe 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -38,6 +38,8 @@ val invalid_arg_loc : loc * string -> 'a
 val todo : string -> unit
 
 exception Timeout
+exception Drop
+exception Quit
 
 (** Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2f129637d..bf0e13e02 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -12,6 +12,7 @@ open Topconstr
 open Glob_term
 open Tacexpr
 open Vernacexpr
+open Locality
 open Pcoq
 open Prim
 open Tactic
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index f86fd0fec..8ec546ffd 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -117,7 +117,7 @@ VERNAC COMMAND EXTEND Admit_Obligations
 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Vernacexpr.use_section_locality ())
+      (Locality.use_section_locality ())
       (Tacinterp.glob_tactic t) ]
 END
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 23e7e31bf..5f44a9e9c 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -13,6 +13,7 @@ open Util
 open Vernac_
 open Topconstr
 open Vernacexpr
+open Locality
 open Prim
 open Constr
 open Tok
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 320ca4eb0..f684b9a0d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Names
 open Topconstr
 open Extend
 open Vernacexpr
+open Locality
 open Pcoq
 open Tactic
 open Decl_kinds
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 0d7cd3649..39fd88506 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -71,7 +71,7 @@ Tacexpr
 Tok
 Lexer
 Extend
-Vernacexpr
+Locality
 Extrawit
 Pcoq
 Q_util
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 48bb87214..a5ee551a5 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -59,7 +59,7 @@ let (set_default_solver, default_solver, print_default_solver) =
 VERNAC COMMAND EXTEND Firstorder_Set_Solver
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
-      (Vernacexpr.use_section_locality ())
+      (Locality.use_section_locality ())
       (Tacinterp.glob_tactic t) ]
 END
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fb9439d73..2700b2b7d 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 458c5bec6..88170d6dd 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 *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 292c288a8..cc3c7c18d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -102,7 +102,7 @@ let coqide_cmd_checks (loc,ast) =
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
     user_error "Use CoqIDE display menu instead";
-  if is_navigation_vernac ast then
+  if Vernac.is_navigation_vernac ast then
     user_error "Use CoqIDE navigation instead";
   if is_undo ast then
     msgerrnl (str "Warning: rather use CoqIDE navigation instead");
@@ -362,8 +362,8 @@ let eval_call c =
         let () = flush !orig_stdout in
         let () = pr_debug "Exiting gracefully." in
         exit 0
-      | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
-      | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
+      | Errors.Drop -> None, "Drop is not allowed by coqide!"
+      | Errors.Quit -> None, "Quit is not allowed by coqide!"
       | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
       | Error_in_file (_,_,inner) -> None, pr_exn inner
       | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
new file mode 100644
index 000000000..436250c92
--- /dev/null
+++ b/toplevel/locality.ml
@@ -0,0 +1,112 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Managing locality *)
+
+let locality_flag = ref None
+
+let local_of_bool = function
+  | true -> Decl_kinds.Local
+  | false -> Decl_kinds.Global
+
+let check_locality () =
+  match !locality_flag with
+  | Some (loc,b) ->
+    let s = if b then "Local" else "Global" in
+    Errors.user_err_loc
+      (loc,"",Pp.str ("This command does not support the \""^s^"\" prefix."))
+  | None -> ()
+
+(** Extracting the locality flag *)
+
+(* Commands which supported an inlined Local flag *)
+
+let enforce_locality_full local =
+  let local =
+    match !locality_flag with
+    | Some (_,false) when local ->
+	Errors.error "Cannot be simultaneously Local and Global."
+    | Some (_,true) when local ->
+	Errors.error "Use only prefix \"Local\"."
+    | None ->
+	if local then begin
+	  Flags.if_warn
+	   Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
+	  Some true
+	end else
+	None
+    | Some (_,b) -> Some b in
+  locality_flag := None;
+  local
+
+(* Commands which did not supported an inlined Local flag (synonym of
+   [enforce_locality_full false]) *)
+
+let use_locality_full () =
+  let r = Option.map snd !locality_flag in
+  locality_flag := None;
+   r
+
+(** Positioning locality for commands supporting discharging and export
+     outside of modules *)
+
+(* For commands whose default is to discharge and export:
+   Global is the default and is neutral;
+   Local in a section deactivates discharge,
+   Local not in a section deactivates export *)
+
+let make_locality = function Some true -> true | _ -> false
+
+let use_locality () = make_locality (use_locality_full ())
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let enforce_locality local = make_locality (enforce_locality_full local)
+
+let enforce_locality_exp local = local_of_bool (enforce_locality local)
+
+(* For commands whose default is not to discharge and not to export:
+   Global forces discharge and export;
+   Local is the default and is neutral *)
+
+let use_non_locality () =
+  match use_locality_full () with Some false -> false | _ -> true
+
+(* For commands whose default is to not discharge but to export:
+   Global in sections forces discharge, Global not in section is the default;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_section_locality =
+  function Some b -> b | None -> Lib.sections_are_opened ()
+
+let use_section_locality () =
+  make_section_locality (use_locality_full ())
+
+let enforce_section_locality local =
+  make_section_locality (enforce_locality_full local)
+
+(** Positioning locality for commands supporting export but not discharge *)
+
+(* For commands whose default is to export (if not in section):
+   Global in sections is forbidden, Global not in section is neutral;
+   Local in sections is the default, Local not in section forces non-export *)
+
+let make_module_locality = function
+  | Some false ->
+      if Lib.sections_are_opened () then
+	Errors.error
+	  "This command does not support the Global option in sections.";
+      false
+  | Some true -> true
+  | None -> false
+
+let use_module_locality () =
+  make_module_locality (use_locality_full ())
+
+let enforce_module_locality local =
+  make_module_locality (enforce_locality_full local)
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
new file mode 100644
index 000000000..5e8d45d87
--- /dev/null
+++ b/toplevel/locality.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Managing locality *)
+
+val locality_flag : (Pp.loc * bool) option ref
+val check_locality : unit -> unit
+
+(** * Extracting the locality flag *)
+
+(** Commands which supported an inlined Local flag *)
+
+val enforce_locality_full : bool -> bool option
+
+(** Commands which did not supported an inlined Local flag
+    (synonym of [enforce_locality_full false]) *)
+
+val use_locality_full : unit -> bool option
+
+(** * Positioning locality for commands supporting discharging and export
+    outside of modules *)
+
+(** For commands whose default is to discharge and export:
+    Global is the default and is neutral;
+    Local in a section deactivates discharge,
+    Local not in a section deactivates export *)
+
+val make_locality : bool option -> bool
+val use_locality : unit -> bool
+val use_locality_exp : unit -> Decl_kinds.locality
+val enforce_locality : bool -> bool
+val enforce_locality_exp : bool -> Decl_kinds.locality
+
+(** For commands whose default is not to discharge and not to export:
+    Global forces discharge and export;
+    Local is the default and is neutral *)
+
+val use_non_locality : unit -> bool
+
+(** For commands whose default is to not discharge but to export:
+    Global in sections forces discharge, Global not in section is the default;
+    Local in sections is the default, Local not in section forces non-export *)
+
+val make_section_locality : bool option -> bool
+val use_section_locality : unit -> bool
+val enforce_section_locality : bool -> bool
+
+(** * Positioning locality for commands supporting export but not discharge *)
+
+(** For commands whose default is to export (if not in section):
+    Global in sections is forbidden, Global not in section is neutral;
+    Local in sections is the default, Local not in section forces non-export *)
+
+val make_module_locality : bool option -> bool
+val use_module_locality : unit -> bool
+val enforce_module_locality : bool -> bool
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 6a06ba3dc..952f80aad 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -12,7 +12,6 @@ open Util
 open Flags
 open Cerrors
 open Vernac
-open Vernacexpr
 open Pcoq
 open Compat
 
@@ -302,11 +301,11 @@ let print_toplevel_error exc =
   match exc with
     | End_of_input ->
 	msgerrnl (mt ()); pp_flush(); exit 0
-    | Vernacexpr.Drop ->  (* Last chance *)
-        if Mltop.is_ocaml_top() then raise Vernacexpr.Drop;
+    | Errors.Drop ->  (* Last chance *)
+        if Mltop.is_ocaml_top() then raise Errors.Drop;
         (str"Error: There is no ML toplevel." ++ fnl ())
-    | Vernacexpr.Quit ->
-	raise Vernacexpr.Quit
+    | Errors.Quit ->
+	raise Errors.Quit
     | _ ->
 	(if is_pervasive_exn exc then (mt ()) else locstrm) ++
         Errors.print exc
@@ -372,9 +371,9 @@ let rec loop () =
     reset_input_buffer stdin top_buffer;
     while true do do_vernac() done
   with
-    | Vernacexpr.Drop -> ()
+    | Errors.Drop -> ()
     | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
-    | Vernacexpr.Quit -> exit 0
+    | Errors.Quit -> exit 0
     | e ->
 	msgerrnl (str"Anomaly. Please report.");
 	loop ()
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index d242036f7..43d15eb43 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,7 +1,7 @@
 Himsg
 Cerrors
 Class
-Vernacexpr
+Locality
 Metasyntax
 Auto_ind_decl
 Libtypes
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 5cb404df7..32387e793 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,6 +27,21 @@ exception DuringCommandInterp of Pp.loc * exn
 
 exception HasNotFailed
 
+(* The navigation vernac commands will be handled separately *)
+
+let rec is_navigation_vernac = function
+  | VernacResetInitial
+  | VernacResetName _
+  | VernacBacktrack _
+  | VernacBackTo _
+  | VernacBack _ -> true
+  | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+  | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
+  | _ -> false
+
 (* Specifies which file is read. The intermediate file names are
    discarded here. The Drop exception becomes an error. We forget
    if the error ocurred during interpretation or not *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 9998fb19c..79ea1a4c5 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -44,3 +44,6 @@ val load_vernac : bool -> string -> unit
 (** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
 
 val compile : bool -> string -> unit
+
+
+val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c12b4e7b..b6e625136 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1626,7 +1626,7 @@ let interp c =
   Flags.program_cmd := false;
   Obligations.set_program_mode isprogcmd;
   try
-    interp c; check_locality ();
+    interp c; Locality.check_locality ();
     Flags.program_mode := mode
   with e ->
     Flags.program_mode := mode;
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index c8d6d87ff..4862419e2 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -14,7 +14,6 @@ open Libnames
 open Himsg
 open Proof_type
 open Tacinterp
-open Vernacexpr
 
 let disable_drop e =
   if e <> Drop then e