More functional implementation of locality_flag and program_mode

This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v)  that represents a vernacular v with the "Local" modifier
- VernacProgram v    that represents a vernacular v with the "Program" modifier

This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST.  This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.

As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag.  In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):

  let local = enforce_XXX_locality locality local in

Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom

  let local = make_XXX_locality locality in

is used to default the locality to XXX (module/section/whatever).

Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
  have an AST, but are parsed as VernacExtend (see vernacinterp.ml)

I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.

Fixing plugins adding commands that honour "Local" should look like this:

 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END

In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.

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

16 files changed, 416 insertions, 349 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 49467a393e..b311b770db 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -121,18 +121,21 @@ type search_restriction =
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
-type locality_flag  = bool (* true = Local;         false = Global         *)
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type inductive_flag = Decl_kinds.recursivity_kind
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
-type full_locality_flag = bool option (* true = Local; false = Global      *)
 type onlyparsing_flag = Flags.compat_version option
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
     which this notation is trying to be compatible with *)
+type locality_flag  = bool (* true = Local *)
+type obsolete_locality = bool
+(* Some grammar entries use obsolete_locality.  This bool is to be backward
+ * compatible.  If the grammar is fixed removing deprecated syntax, this
+ * bool should go away too *)
 
 type option_value = Interface.option_value =
   | BoolValue of bool
@@ -249,28 +252,33 @@ type vernac_expr =
 
   (* Syntax *)
   | VernacTacticNotation of
-      locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr
-  | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
-  | VernacOpenCloseScope of (locality_flag * bool * scope_name)
+      int * grammar_tactic_prod_item_expr list * raw_tactic_expr
+  | VernacSyntaxExtension of
+      obsolete_locality * (lstring * syntax_modifier list)
+  | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
   | VernacDelimiters of scope_name * string
   | VernacBindScope of scope_name * reference or_by_notation list
-  | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
+  | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of
-      locality_flag * constr_expr * (lstring * syntax_modifier list) *
+      obsolete_locality * constr_expr * (lstring * syntax_modifier list) *
       scope_name option
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * lident * definition_expr
+  | VernacDefinition of
+      (locality option * definition_object_kind) * lident * definition_expr
   | VernacStartTheoremProof of theorem_kind *
       (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
         bool
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
+  | VernacAssumption of (locality option * assumption_object_kind) *
+      inline * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of locality * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of locality * (cofixpoint_expr * decl_notation list) list
+  | VernacFixpoint of
+      locality option * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of
+      locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
 
@@ -281,15 +289,14 @@ type vernac_expr =
       export_flag option * lreference list
   | VernacImport of export_flag * lreference list
   | VernacCanonical of reference or_by_notation
-  | VernacCoercion of locality_flag * reference or_by_notation *
+  | VernacCoercion of obsolete_locality * reference or_by_notation *
       class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of locality_flag * lident *
+  | VernacIdentityCoercion of obsolete_locality * lident *
       class_rawexpr * class_rawexpr
 
   (* Type classes *)
   | VernacInstance of
       bool * (* abstract instance *)
-      bool * (* global *)
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	constr_expr option * (* props *)
@@ -297,8 +304,7 @@ type vernac_expr =
 
   | VernacContext of local_binder list
 
-  | VernacDeclareInstances of
-      bool (* global *) * reference list (* instance names *)
+  | VernacDeclareInstances of reference list (* instance names *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)
 
@@ -321,7 +327,7 @@ type vernac_expr =
   | VernacAddLoadPath of rec_flag * string * DirPath.t option
   | VernacRemoveLoadPath of string
   | VernacAddMLPath of rec_flag * string
-  | VernacDeclareMLModule of locality_flag * string list
+  | VernacDeclareMLModule of string list
   | VernacChdir of string option
 
   (* State management *)
@@ -336,33 +342,34 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
-  | VernacCreateHintDb of locality_flag * string * bool
-  | VernacRemoveHints of locality_flag * string list * reference list
-  | VernacHints of locality_flag * string list * hints_expr
+      (rec_flag * (reference * bool * raw_tactic_expr) list)
+  | VernacCreateHintDb of string * bool
+  | VernacRemoveHints of string list * reference list
+  | VernacHints of obsolete_locality * string list * hints_expr
   | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
-      locality_flag * onlyparsing_flag
-  | VernacDeclareImplicits of locality_flag * reference or_by_notation *
+      obsolete_locality * onlyparsing_flag
+  | VernacDeclareImplicits of reference or_by_notation *
       (explicitation * bool * bool) list list
-  | VernacArguments of locality_flag * reference or_by_notation *
+  | VernacArguments of reference or_by_notation *
       ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
       int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
-  | VernacArgumentsScope of locality_flag * reference or_by_notation *
+  | VernacArgumentsScope of reference or_by_notation *
       scope_name option list
   | VernacReserve of simple_binder list
-  | VernacGeneralizable of locality_flag * (lident list) option
-  | VernacSetOpacity of
-      locality_flag * (Conv_oracle.level * reference or_by_notation list) list
-  | VernacUnsetOption of full_locality_flag * Goptions.option_name
-  | VernacSetOption of full_locality_flag * Goptions.option_name * option_value
+  | VernacGeneralizable of (lident list) option
+  | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
+  | VernacSetStrategy of
+      (Conv_oracle.level * reference or_by_notation list) list
+  | VernacUnsetOption of Goptions.option_name
+  | VernacSetOption of Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
   | VernacPrintOption of Goptions.option_name
   | VernacCheckMayEval of raw_red_expr option * int option * constr_expr
   | VernacGlobalCheck of constr_expr
-  | VernacDeclareReduction of locality_flag * string * raw_red_expr
+  | VernacDeclareReduction of string * raw_red_expr
   | VernacPrint of printable
   | VernacSearch of searchable * search_restriction
   | VernacLocate of locatable
@@ -393,4 +400,8 @@ type vernac_expr =
   (* For extension *)
   | VernacExtend of string * raw_generic_argument list
 
+  (* Flags *)
+  | VernacProgram of vernac_expr
+  | VernacLocal of bool * vernac_expr
+
 and located_vernac_expr = Loc.t * vernac_expr
diff --git a/lib/flags.ml b/lib/flags.ml
index bd31b40248..6c67cb237f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -84,11 +84,6 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
-(** [program_cmd] indicates that the current command is a Program one.
-    [program_mode] tells that Program mode has been activated, either
-    globally via [Set Program] or locally via the Program command prefix. *)
-
-let program_cmd = ref false
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 6b26c50d9e..6325d7cd44 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,11 +52,6 @@ val is_auto_intros : unit -> bool
 val make_term_color : bool -> unit
 val is_term_color : unit -> bool
 
-(** [program_cmd] indicates that the current command is a Program one.
-    [program_mode] tells that Program mode has been activated, either
-    globally via [Set Program] or locally via the Program command prefix. *)
-
-val program_cmd : bool ref
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 4c863ee67e..20fe3af643 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -107,7 +107,7 @@ VERNAC COMMAND EXTEND Admit_Obligations
 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 194ed59262..3090fd7f32 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -83,17 +83,17 @@ GEXTEND Gram
       (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
-	    VernacCreateHintDb (use_module_locality (), id, b)
+	    VernacCreateHintDb (id, b)
       | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
-	  VernacRemoveHints (use_module_locality (), dbnames, ids)
+	  VernacRemoveHints (dbnames, ids)
       | IDENT "Hint"; local = obsolete_locality; h = hint;
 	  dbnames = opt_hintbases ->
-	  VernacHints (enforce_module_locality local,dbnames, h)
+	  VernacHints (local,dbnames, h)
       (* Declare "Resolve" explicitly so as to be able to later extend with
          "Resolve ->" and "Resolve <-" *)
       | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural;
 	  dbnames = opt_hintbases ->
-	  VernacHints (use_module_locality (),dbnames,
+	  VernacHints (false,dbnames,
 	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
       ] ];
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5787186ad0..56abf3e1c4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -74,15 +74,18 @@ GEXTEND Gram
     [ [ IDENT "Time"; v = vernac -> VernacTime v
       | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
       | IDENT "Fail"; v = vernac -> VernacFail v
-      | locality; v = vernac_aux -> v ] ]
+      | IDENT "Local"; v = vernac_aux -> VernacLocal (true, v)
+      | IDENT "Global"; v = vernac_aux -> VernacLocal (false, v)
+      | v = vernac_aux -> v ] 
+    ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> Flags.program_cmd := true; g
-      | IDENT "Program"; g = gallina_ext; "." -> Flags.program_cmd := true; g
-      | g = gallina; "." -> Flags.program_cmd := false; g
-      | g = gallina_ext; "." -> Flags.program_cmd := false; g
+    [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g
+      | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g
+      | g = gallina; "." -> g
+      | g = gallina_ext; "." -> g
       | c = command; "." -> c
       | c = syntax; "." -> c
       | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
@@ -92,11 +95,6 @@ GEXTEND Gram
   vernac_aux: LAST
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
-  locality:
-    [ [ IDENT "Local" -> locality_flag := Some (!@loc,true)
-      | IDENT "Global" -> locality_flag := Some (!@loc,false)
-      | -> locality_flag := None ] ]
-  ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
@@ -162,7 +160,7 @@ GEXTEND Gram
       | d = def_token; id = identref; b = def_body ->
           VernacDefinition (d, id, b)
       | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((Discharge, Definition), id, b)
+          VernacDefinition ((Some Discharge, Definition), id, b)
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -170,13 +168,13 @@ GEXTEND Gram
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (f,false,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (use_locality_exp (), recs)
+          VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (Discharge, recs)
+          VernacFixpoint (Some Discharge, recs)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (use_locality_exp (), corecs)
+          VernacCoFixpoint (None, corecs)
       | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (Discharge, corecs)
+          VernacCoFixpoint (Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
@@ -201,25 +199,22 @@ GEXTEND Gram
       | IDENT "Property" -> Property ] ]
   ;
   def_token:
-    [ [ "Definition" ->
-	(use_locality_exp (), Definition)
-      | IDENT "Example" ->
-	(use_locality_exp (), Example)
-      | IDENT "SubClass"  ->
-        (use_locality_exp (), SubClass) ] ]
+    [ [ "Definition" -> (None, Definition)
+      | IDENT "Example" -> (None, Example)
+      | IDENT "SubClass" -> (None, SubClass) ] ]
   ;
   assumption_token:
-    [ [ "Hypothesis" -> (Discharge, Logical)
-      | "Variable" -> (Discharge, Definitional)
-      | "Axiom" -> (use_locality_exp (), Logical)
-      | "Parameter" -> (use_locality_exp (), Definitional)
-      | IDENT "Conjecture" -> (use_locality_exp (), Conjectural) ] ]
+    [ [ "Hypothesis" -> (Some Discharge, Logical)
+      | "Variable" -> (Some Discharge, Definitional)
+      | "Axiom" -> (None, Logical)
+      | "Parameter" -> (None, Definitional)
+      | IDENT "Conjecture" -> (None, Conjectural) ] ]
   ;
   assumptions_token:
-    [ [ IDENT "Hypotheses" -> (Discharge, Logical)
-      | IDENT "Variables" -> (Discharge, Definitional)
-      | IDENT "Axioms" -> (use_locality_exp (), Logical)
-      | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ]
+    [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
+      | IDENT "Variables" -> (Some Discharge, Definitional)
+      | IDENT "Axioms" -> (None, Logical)
+      | IDENT "Parameters" -> (None, Definitional) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
@@ -522,12 +517,12 @@ GEXTEND Gram
   gallina_ext:
     [ [ (* Transparent and Opaque *)
         IDENT "Transparent"; l = LIST1 smart_global ->
-          VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l])
+          VernacSetOpacity (Conv_oracle.transparent, l)
       | IDENT "Opaque"; l = LIST1 smart_global ->
-          VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l])
+          VernacSetOpacity (Conv_oracle.Opaque, l)
       | IDENT "Strategy"; l =
-          LIST1 [ lev=strategy_level; "["; q=LIST1 smart_global; "]" -> (lev,q)] ->
-            VernacSetOpacity (use_locality (),l)
+          LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] ->
+            VernacSetStrategy l
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical (AN qid)
@@ -537,33 +532,33 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Global,CanonicalStructure),(Loc.ghost,s),d)
+	    ((Some Global,CanonicalStructure),(Loc.ghost,s),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((None,Coercion),(Loc.ghost,s),d)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d)
+	  VernacDefinition ((Some Decl_kinds.Local,Coercion),(Loc.ghost,s),d)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
-	   VernacIdentityCoercion (enforce_locality true, f, s, t)
+	   VernacIdentityCoercion (true, f, s, t)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
-	   VernacIdentityCoercion (use_locality (), f, s, t)
+	   VernacIdentityCoercion (false, f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (enforce_locality true, AN qid, s, t)
+	  VernacCoercion (true, AN qid, s, t)
       | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (enforce_locality true, ByNotation ntn, s, t)
+	  VernacCoercion (true, ByNotation ntn, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (use_locality (), AN qid, s, t)
+	  VernacCoercion (false, AN qid, s, t)
       | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (use_locality (), ByNotation ntn, s, t)
+	  VernacCoercion (false, ByNotation ntn, s, t)
 
       | IDENT "Context"; c = binders ->
 	  VernacContext c
@@ -573,13 +568,12 @@ GEXTEND Gram
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> Some r |
 	     ":="; c = lconstr -> Some c | -> None ] ->
-	   VernacInstance (false, not (use_section_locality ()),
-			   snd namesup, (fst namesup, expl, t), props, pri)
+	   VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri)
 
       | IDENT "Existing"; IDENT "Instance"; id = global ->
-	  VernacDeclareInstances (not (use_section_locality ()), [id])
+	  VernacDeclareInstances [id]
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global ->
-	  VernacDeclareInstances (not (use_section_locality ()), ids)
+	  VernacDeclareInstances ids
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
@@ -623,14 +617,14 @@ GEXTEND Gram
          if List.mem `SimplNeverUnfold mods &&
             List.mem `SimplDontExposeCase mods then
            err_incompat "simpl never" "simpl nomatch";
-         VernacArguments (use_section_locality(), qid, impl, nargs, mods)
+         VernacArguments (qid, impl, nargs, mods)
 
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
 	   Flags.if_verbose
              msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
-	 VernacArgumentsScope (use_section_locality (),qid,scl)
+	 VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
@@ -638,7 +632,7 @@ GEXTEND Gram
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   Flags.if_verbose
              msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead");
-	   VernacDeclareImplicits (use_section_locality (),qid,pos)
+	   VernacDeclareImplicits (qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
 	   VernacReserve bl
@@ -652,7 +646,7 @@ GEXTEND Gram
 	     | IDENT "No"; IDENT "Variables" -> None
 	     | ["Variable" | IDENT "Variables"];
 		  idl = LIST1 identref -> Some idl ] ->
-	     VernacGeneralizable (use_non_locality (), gen) ] ]
+	     VernacGeneralizable gen ] ]
   ;
   arguments_modifier:
     [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
@@ -713,7 +707,7 @@ GEXTEND Gram
   command:
     [ [ IDENT "Ltac";
         l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition (use_module_locality (), true, l)
+          VernacDeclareTacticDefinition (true, l)
 
       | IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
@@ -721,9 +715,7 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ->
-	   VernacInstance (true, not (use_section_locality ()),
-			   snd namesup, (fst namesup, expl, t),
-			   None, pri)
+	   VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri)
 
       (* System directory *)
       | IDENT "Pwd" -> VernacChdir None
@@ -738,7 +730,7 @@ GEXTEND Gram
 	s = [ s = ne_string -> s | s = IDENT -> s ] ->
 	  VernacLoad (verbosely, s)
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
-	  VernacDeclareMLModule (use_locality (), l)
+	  VernacDeclareMLModule l
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
@@ -793,11 +785,11 @@ GEXTEND Gram
 
       (* Pour intervenir sur les tables de paramčtres *)
       | "Set"; table = option_table; v = option_value ->
-  	  VernacSetOption (use_locality_full(),table,v)
+  	  VernacSetOption (table,v)
       | "Set"; table = option_table ->
-  	  VernacSetOption (use_locality_full(),table,BoolValue true)
+  	  VernacSetOption (table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
-  	  VernacUnsetOption (use_locality_full(),table)
+  	  VernacUnsetOption table
 
       | IDENT "Print"; IDENT "Table"; table = option_table ->
 	  VernacPrintOption table
@@ -951,16 +943,16 @@ GEXTEND Gram
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" ->
-          VernacSetOption (None,["Ltac";"Debug"], BoolValue true)
+          VernacSetOption (["Ltac";"Debug"], BoolValue true)
 
       |	IDENT "Debug"; IDENT "Off" ->
-          VernacSetOption (None,["Ltac";"Debug"], BoolValue false)
+          VernacSetOption (["Ltac";"Debug"], BoolValue false)
 
 (* registration of a custom reduction *)
 
       | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
          r = Tactic.red_expr ->
-	   VernacDeclareReduction (use_locality(),s,r)
+	   VernacDeclareReduction (s,r)
 
  ] ];
     END
@@ -973,10 +965,10 @@ GEXTEND Gram
 
   syntax:
    [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (enforce_section_locality local,true,sc)
+         VernacOpenCloseScope (local,(true,sc))
 
      | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (enforce_section_locality local,false,sc)
+         VernacOpenCloseScope (local,(false,sc))
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -988,31 +980,31 @@ GEXTEND Gram
 	 op = ne_lstring; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (enforce_module_locality local,(op,modl),p,sc)
+         VernacInfix (local,(op,modl),p,sc)
      | IDENT "Notation"; local = obsolete_locality; id = identref;
 	 idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            VernacSyntacticDefinition
-	     (id,(idl,c),enforce_module_locality local,b)
+	     (id,(idl,c),local,b)
      | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":=";
 	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (enforce_module_locality local,c,(s,modl),sc)
+           VernacNotation (local,c,(s,modl),sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level;
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticNotation (use_module_locality(),n,pil,t)
+         -> VernacTacticNotation (n,pil,t)
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   Metasyntax.check_infix_modifiers l;
 	   let (loc,s) = s in
-	   VernacSyntaxExtension (use_module_locality(),((loc,"x '"^s^"' y"),l))
+	   VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l))
 
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
 	 s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (enforce_module_locality local,(s,l))
+	 -> VernacSyntaxExtension (local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order
         to factorize with other "Print"-based vernac entries *)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 0cb45f51d4..bdea8b1a93 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -56,7 +56,7 @@ let (set_default_solver, default_solver, print_default_solver) =
 VERNAC COMMAND EXTEND Firstorder_Set_Solver
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 572876e5bf..415d703162 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -177,7 +177,7 @@ let pr_reference_or_constr pr_c = function
   | HintsReference r -> pr_reference r
   | HintsConstr c -> pr_c c
 
-let pr_hints local db h pr_c pr_pat =
+let pr_hints db h pr_c pr_pat =
   let opth = pr_opt_hintbases db  in
   let pph =
     match h with
@@ -200,7 +200,7 @@ let pr_hints local db h pr_c pr_pat =
           str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
           spc() ++ pr_raw_tactic tac
   in
-  hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
+  hov 2 (str"Hint "++ pph ++ opth)
 
 let pr_with_declaration pr_c = function
   | CWith_Definition (id,c) ->
@@ -306,7 +306,9 @@ let pr_class_rawexpr = function
   | SortClass -> str"Sortclass"
   | RefClass qid -> pr_smart_global qid
 
-let pr_assumption_token many = function
+let pr_assumption_token many (l,a) =
+  let l = match l with Some x -> x | None -> Decl_kinds.Global in
+  match l, a with
   | (Discharge,Logical) ->
       str (if many then "Hypotheses" else "Hypothesis")
   | (Discharge,Definitional) ->
@@ -475,6 +477,8 @@ let pr_printable = function
 in
 
 let rec pr_vernac = function
+  | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
+  | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
 
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
@@ -530,10 +534,9 @@ let rec pr_vernac = function
   | VernacFail v -> str"Fail" ++ spc() ++ pr_vernac v
 
   (* Syntax *)
-  | VernacTacticNotation (local,n,r,e) ->
-      pr_locality local ++ pr_grammar_tactic_rule n ("",r,e)
-  | VernacOpenCloseScope (local,opening,sc) ->
-      pr_section_locality local ++
+  | VernacTacticNotation (n,r,e) ->
+      pr_grammar_tactic_rule n ("",r,e)
+  | VernacOpenCloseScope (_,(opening,sc)) ->
       str (if opening then "Open " else "Close ") ++
       str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
@@ -542,20 +545,20 @@ let rec pr_vernac = function
   | VernacBindScope (sc,cll) ->
       str"Bind Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
-  | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
+  | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function
       |	None -> str"_"
       |	Some sc -> str sc in
-    pr_section_locality local ++ str"Arguments Scope" ++ spc() ++
+    str"Arguments Scope" ++ spc() ++
     pr_smart_global q
     ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-  | VernacInfix (local,((_,s),mv),q,sn) -> (* A Verifier *)
-      hov 0 (hov 0 (pr_locality local ++ str"Infix "
+  | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+      hov 0 (hov 0 (str"Infix "
       ++ qs s ++ str " :=" ++ pr_constrarg q) ++
       pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacNotation (local,c,((_,s),l),opt) ->
+  | VernacNotation (_,c,((_,s),l),opt) ->
       let ps =
 	let n = String.length s in
 	if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
@@ -563,18 +566,20 @@ let rec pr_vernac = function
           let s' = String.sub s 1 (n-2) in
           if String.contains s' '\'' then qs s else str s'
 	else qs s in
-      hov 2 (pr_locality local ++ str"Notation" ++ spc() ++ ps ++
+      hov 2 (str"Notation" ++ spc() ++ ps ++
       str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
-  | VernacSyntaxExtension (local,(s,l)) ->
-      pr_locality local ++ str"Reserved Notation" ++ spc() ++ pr_located qs s ++
+  | VernacSyntaxExtension (_,(s,l)) ->
+      str"Reserved Notation" ++ spc() ++ pr_located qs s ++
       pr_syntax_modifiers l
 
   (* Gallina *)
   | VernacDefinition (d,id,b) -> (* A verifier... *)
-      let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
+      let pr_def_token (l,dk) =
+        let l = match l with Some x -> x | None -> Decl_kinds.Global in
+        str (Kindops.string_of_definition_kind (l,dk)) in
       let pr_reduce = function
         | None -> mt()
         | Some r ->
@@ -650,9 +655,9 @@ let rec pr_vernac = function
 
   | VernacFixpoint (local, recs) ->
       let local = match local with
-      | Discharge -> "Let "
-      | Local -> "Local "
-      | Global -> ""
+      | Some Discharge -> "Let "
+      | Some Local -> "Local "
+      | None | Some Global -> ""
       in
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
@@ -667,9 +672,9 @@ let rec pr_vernac = function
 
   | VernacCoFixpoint (local, corecs) ->
       let local = match local with
-      | Discharge -> "Let "
-      | Local -> "Local "
-      | Global -> ""
+      | Some Discharge -> "Let "
+      | Some Local -> "Local "
+      | None | Some Global -> ""
       in
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -698,22 +703,19 @@ let rec pr_vernac = function
       (if f then str"Export" else str"Import") ++ spc() ++
       prlist_with_sep sep pr_import_module l
   | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q
-  | VernacCoercion (s,id,c1,c2) ->
+  | VernacCoercion (_,id,c1,c2) ->
       hov 1 (
-	str"Coercion" ++ (if s then spc() ++
-	  str"Local" ++ spc() else spc()) ++
+	str"Coercion" ++
 	pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
 	spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
-  | VernacIdentityCoercion (s,id,c1,c2) ->
+  | VernacIdentityCoercion (_,id,c1,c2) ->
       hov 1 (
-	str"Identity Coercion" ++ (if s then spc() ++
-	  str"Local" ++ spc() else spc()) ++ pr_lident id ++
+	str"Identity Coercion" ++ pr_lident id ++
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
- | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
-       pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
        str"Instance" ++
        (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () |
@@ -730,10 +732,10 @@ let rec pr_vernac = function
        str"Context" ++ spc () ++ pr_and_type_binders_arg l)
 
 
- | VernacDeclareInstances (glob, ids) ->
-     hov 1 (pr_non_locality (not glob) ++
-               str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++
-               spc () ++ prlist_with_sep spc pr_reference ids)
+ | VernacDeclareInstances ids ->
+     hov 1 ( str"Existing" ++ spc () ++ 
+             str(String.plural (List.length ids) "Instance") ++
+             spc () ++ prlist_with_sep spc pr_reference ids)
 
  | VernacDeclareClass id ->
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
@@ -784,13 +786,12 @@ let rec pr_vernac = function
   | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s
   | VernacAddMLPath (fl,s) ->
       str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s
-  | VernacDeclareMLModule (local, l) ->
-      pr_locality local ++
+  | VernacDeclareMLModule (l) ->
       hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
   | VernacChdir s -> str"Cd" ++ pr_opt qs s
 
   (* Commands *)
-  | VernacDeclareTacticDefinition (local,rc,l) ->
+  | VernacDeclareTacticDefinition (rc,l) ->
       let pr_tac_body (id, redef, body) =
         let idl, body =
           match body with
@@ -803,34 +804,33 @@ let rec pr_vernac = function
         pr_raw_tactic body
       in
       hov 1
-        (pr_locality local ++ str "Ltac " ++
+        (str "Ltac " ++
         prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l)
-  | VernacCreateHintDb (local,dbname,b) ->
-      hov 1 (pr_locality local ++ str "Create HintDb " ++
+  | VernacCreateHintDb (dbname,b) ->
+      hov 1 (str "Create HintDb " ++
 		str dbname ++ (if b then str" discriminated" else mt ()))
-  | VernacRemoveHints (local, dbnames, ids) ->
-      hov 1 (pr_locality local ++ str "Remove Hints " ++
+  | VernacRemoveHints (dbnames, ids) ->
+      hov 1 (str "Remove Hints " ++
 	       prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
 	       pr_opt_hintbases dbnames)
-  | VernacHints (local,dbnames,h) ->
-      pr_hints local dbnames h pr_constr pr_constr_pattern_expr
-  | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
+  | VernacHints (_, dbnames,h) ->
+      pr_hints dbnames h pr_constr pr_constr_pattern_expr
+  | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
       hov 2
-        (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+        (str"Notation " ++ pr_lident id ++ spc () ++
 	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
          pr_syntax_modifiers
 	   (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
-  | VernacDeclareImplicits (local,q,[]) ->
-      hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
-	pr_smart_global q)
-  | VernacDeclareImplicits (local,q,impls) ->
-      hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++
+  | VernacDeclareImplicits (q,[]) ->
+      hov 2 (str"Implicit Arguments" ++ spc() ++ pr_smart_global q)
+  | VernacDeclareImplicits (q,impls) ->
+      hov 1 (str"Implicit Arguments " ++
 	spc() ++ pr_smart_global q ++ spc() ++
 	prlist_with_sep spc (fun imps ->
 	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
 	  impls)
-  | VernacArguments (local, q, impl, nargs, mods) ->
-      hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+  | VernacArguments (q, impl, nargs, mods) ->
+      hov 2 (str"Arguments" ++ spc() ++
         pr_smart_global q ++
       let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
       let pr_if b x = if b then x else str "" in
@@ -861,21 +861,23 @@ let rec pr_vernac = function
       hov 2 (str"Implicit Type" ++
         str (if n > 1 then "s " else " ") ++
         pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
-  | VernacGeneralizable (local, g) ->
-      hov 1 (pr_locality local ++ str"Generalizable Variable" ++
+  | VernacGeneralizable g ->
+      hov 1 (str"Generalizable Variable" ++
 		match g with
 		| None -> str "s none"
 		| Some [] -> str "s all"
 		| Some idl ->
 		    str (if List.length idl > 1 then "s " else " ") ++
 		      prlist_with_sep spc pr_lident idl)
-  | VernacSetOpacity(b,[k,l]) when Conv_oracle.is_transparent k ->
-      hov 1 (pr_non_locality b ++ str "Transparent" ++
+  | VernacSetOpacity(k,l) when Conv_oracle.is_transparent k ->
+      hov 1 (str "Transparent" ++
              spc() ++ prlist_with_sep sep pr_smart_global l)
-  | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
-      hov 1 (pr_non_locality b ++ str "Opaque" ++
+  | VernacSetOpacity(Conv_oracle.Opaque,l) ->
+      hov 1 (str "Opaque" ++
              spc() ++ prlist_with_sep sep pr_smart_global l)
-  | VernacSetOpacity (local,l) ->
+  | VernacSetOpacity _ ->
+      Errors.anomaly (str "VernacSetOpacity used to set something else")
+  | VernacSetStrategy l ->
       let pr_lev = function
           Conv_oracle.Opaque -> str"opaque"
         | Conv_oracle.Expand -> str"expand"
@@ -884,12 +886,12 @@ let rec pr_vernac = function
       let pr_line (l,q) =
         hov 2 (pr_lev l ++ spc() ++
                str"[" ++ prlist_with_sep sep pr_smart_global q ++ str"]") in
-      hov 1 (pr_locality local ++ str "Strategy" ++ spc() ++
+      hov 1 (str "Strategy" ++ spc() ++
              hv 0 (prlist_with_sep sep pr_line l))
-  | VernacUnsetOption (l,na) ->
-      hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)
-  | VernacSetOption (l,na,v) ->
-      hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v)
+  | VernacUnsetOption (na) ->
+      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (na,v) ->
+      hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
   | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
   | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
   | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
@@ -905,8 +907,8 @@ let rec pr_vernac = function
       let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
       pr_i ++ pr_mayeval r c
   | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
-  | VernacDeclareReduction (b,s,r) ->
-     pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
+  | VernacDeclareReduction (s,r) ->
+     str "Declare Reduction " ++ str s ++ str " := " ++
      pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
   | VernacPrint p -> pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 1be29aefe6..713d6f233a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -603,6 +603,6 @@ END
 VERNAC COMMAND EXTEND HintCut
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
   let entry = HintsCutEntry p in
-    Auto.add_hints (Locality.use_section_locality ())
+    Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (match dbnames with None -> ["core"] | Some l -> l) entry ]
 END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index ad8517c32a..dc59005f68 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1606,7 +1606,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 (Locality.use_section_locality ()) in
+  let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) 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
@@ -1864,16 +1864,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 (Locality.use_section_locality ())) [] a aeq t n ]
+     [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ]
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [	add_setoid (not (Locality.use_section_locality ())) binders a aeq t n ]
+     [	add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ add_morphism_infer (not (Locality.use_section_locality ())) m n ]
+      [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Locality.use_section_locality ())) [] m s n ]
+      [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
 	"with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Locality.use_section_locality ())) binders m s n ]
+      [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
 END
 
 (** Bind to "rewrite" too *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 6e7ed6e7fc..681f0f2c86 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -74,12 +74,12 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Universes"]]
 
 let is_known_option cmd = match cmd with
-  | VernacSetOption (_,o,BoolValue true)
-  | VernacUnsetOption (_,o) -> coqide_known_option o
+  | VernacSetOption (o,BoolValue true)
+  | VernacUnsetOption o -> coqide_known_option o
   | _ -> false
 
 let is_debug cmd = match cmd with
-  | VernacSetOption (_,["Ltac";"Debug"], _) -> true
+  | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
 let is_query cmd = match cmd with
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 88c3b3c056..49478cb261 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -8,30 +8,27 @@
 
 (** * 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 check_locality locality_flag =
+  match locality_flag with
+  | Some 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."))
+    Errors.error ("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 enforce_locality_full locality_flag local =
   let local =
-    match !locality_flag with
-    | Some (_,false) when local ->
+    match locality_flag with
+    | Some false when local ->
 	Errors.error "Cannot be simultaneously Local and Global."
-    | Some (_,true) when local ->
+    | Some true when local ->
 	Errors.error "Use only prefix \"Local\"."
     | None ->
 	if local then begin
@@ -40,18 +37,9 @@ let enforce_locality_full local =
 	  Some true
 	end else
 	None
-    | Some (_,b) -> Some b in
-  locality_flag := None;
+    | Some b -> Some b in
   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 *)
 
@@ -59,23 +47,19 @@ let use_locality_full () =
    Global is the default and is neutral;
    Local in a section deactivates discharge,
    Local not in a section deactivates export *)
+let make_non_locality = function Some false -> false | _ -> true
 
 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 locality_flag local =
+   make_locality (enforce_locality_full locality_flag 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
+let enforce_locality_exp locality_flag local =
+  match locality_flag, local with
+  | None, Some local -> local
+  | Some b, None -> local_of_bool b
+  | None, None -> Decl_kinds.Global
+  | Some _, Some _ -> Errors.error "Local non allowed in this case"
 
 (* For commands whose default is to not discharge but to export:
    Global in sections forces discharge, Global not in section is the default;
@@ -84,11 +68,8 @@ let use_non_locality () =
 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)
+let enforce_section_locality locality_flag local =
+  make_section_locality (enforce_locality_full locality_flag local)
 
 (** Positioning locality for commands supporting export but not discharge *)
 
@@ -105,8 +86,15 @@ let make_module_locality = function
   | 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)
+let enforce_module_locality locality_flag local =
+  make_module_locality (enforce_locality_full locality_flag local)
+
+module LocalityFixme = struct
+  let locality = ref None
+  let set l = locality := l
+  let consume () =
+    let l = !locality in
+    locality := None;
+    l
+  let assert_consumed () = check_locality !locality
+end
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
index b63378ed14..d98c9fa88f 100644
--- a/toplevel/locality.mli
+++ b/toplevel/locality.mli
@@ -8,19 +8,9 @@
 
 (** * Managing locality *)
 
-val locality_flag : (Loc.t * 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
+val enforce_locality_full : bool option -> bool -> bool option
 
 (** * Positioning locality for commands supporting discharging and export
     outside of modules *)
@@ -31,24 +21,17 @@ val use_locality_full : unit -> bool option
     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
+val make_non_locality : bool option -> bool
+val enforce_locality : bool option -> bool -> bool
+val enforce_locality_exp :
+  bool option -> Decl_kinds.locality option -> Decl_kinds.locality
 
 (** 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
+val enforce_section_locality : bool option -> bool -> bool
 
 (** * Positioning locality for commands supporting export but not discharge *)
 
@@ -57,5 +40,12 @@ val enforce_section_locality : bool -> bool
     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
+val enforce_module_locality : bool option -> bool -> bool
+
+(* This is the old imperative interface that is still used for
+ * VernacExtend vernaculars.  Time permitting this could be trashed too *)
+module LocalityFixme : sig
+  val set : bool option -> unit
+  val consume : unit -> bool option
+  val assert_consumed : unit -> unit
+end
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d713fdcc28..a3aa6607e8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -32,6 +32,7 @@ open Redexpr
 open Lemmas
 open Declaremods
 open Misctypes
+open Locality
 
 (* Misc *)
 
@@ -433,27 +434,35 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension = Metasyntax.add_syntax_extension
+let vernac_syntax_extension locality local =
+  let local = enforce_module_locality locality local in
+  Metasyntax.add_syntax_extension local
 
 let vernac_delimiters = Metasyntax.add_delimiters
 
 let vernac_bind_scope sc cll =
   Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
 
-let vernac_open_close_scope = Notation.open_close_scope
+let vernac_open_close_scope locality local (b,s) =
+  let local = enforce_section_locality locality local in
+  Notation.open_close_scope (local,b,s)
 
-let vernac_arguments_scope local r scl =
+let vernac_arguments_scope locality r scl =
+  let local = make_section_locality locality in
   Notation.declare_arguments_scope local (smart_global r) scl
 
-let vernac_infix = Metasyntax.add_infix
+let vernac_infix locality local =
+  let local = enforce_module_locality locality local in
+  Metasyntax.add_infix local
 
-let vernac_notation = Metasyntax.add_notation
+let vernac_notation locality local =
+  let local = enforce_module_locality locality local in
+  Metasyntax.add_notation local
 
 (***********)
 (* Gallina *)
 
 let start_proof_and_print k l hook =
-  Locality.check_locality (); (* early check, cf #2975 *)
   start_proof_com k l hook;
   print_subgoals ()
 
@@ -465,7 +474,8 @@ let vernac_definition_hook = function
 | SubClass -> Class.add_subclass_hook
 | _ -> no_hook
 
-let vernac_definition (local,k) (loc,id as lid) def =
+let vernac_definition locality (local,k) (loc,id as lid) def =
+  let local = enforce_locality_exp locality local in
   let hook = vernac_definition_hook k in
   let () = match local with
   | Discharge -> Dumpglob.dump_definition lid true "var"
@@ -523,8 +533,10 @@ let vernac_exact_proof c =
   save_named true;
   Backtrack.mark_unreachable [prf]
 
-let vernac_assumption kind l nl=
-  let global = (fst kind) == Global in
+let vernac_assumption locality (local, kind) l nl=
+  let local = enforce_locality_exp locality local in
+  let global = local == Global in
+  let kind = local, kind in
   let status =
     List.fold_left (fun status (is_coe,(idl,c)) ->
       if Dumpglob.dump () then
@@ -582,12 +594,14 @@ let vernac_inductive finite infer indl =
     let indl = List.map unpack indl in
     do_mutual_inductive indl (finite != CoFinite)
 
-let vernac_fixpoint local l =
+let vernac_fixpoint locality local l =
+  let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_fixpoint local l
 
-let vernac_cofixpoint local l =
+let vernac_cofixpoint locality local l =
+  let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint local l
@@ -774,28 +788,32 @@ let vernac_require import qidl =
 let vernac_canonical r =
   Recordops.declare_canonical_structure (smart_global r)
 
-let vernac_coercion stre ref qids qidt =
+let vernac_coercion locality local ref qids qidt =
+  let local = enforce_locality locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' ~local:stre ~source ~target;
+  Class.try_add_new_coercion_with_target ref' ~local ~source ~target;
   if_verbose msg_info (pr_global ref' ++ str " is now a coercion")
 
-let vernac_identity_coercion stre id qids qidt =
+let vernac_identity_coercion locality local id qids qidt =
+  let local = enforce_locality locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id ~local:stre ~source ~target
+  Class.try_add_new_identity_coercion id ~local ~source ~target
 
 (* Type classes *)
 
-let vernac_instance abst glob sup inst props pri =
+let vernac_instance abst locality sup inst props pri =
+  let glob = not (make_section_locality locality) in
   Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
 
 let vernac_context l =
   if not (Classes.context l) then raise UnsafeSuccess
 
-let vernac_declare_instances glob ids =
+let vernac_declare_instances locality ids =
+  let glob = not (make_section_locality locality) in
   List.iter (fun (id) -> Classes.existing_instance glob id) ids
 
 let vernac_declare_class id =
@@ -870,7 +888,8 @@ let vernac_remove_loadpath path =
 let vernac_add_ml_path isrec path =
   (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path)
 
-let vernac_declare_ml_module local l =
+let vernac_declare_ml_module locality l =
+  let local = make_locality locality in
   Mltop.declare_ml_modules local (List.map expand l)
 
 let vernac_chdir = function
@@ -897,30 +916,37 @@ let vernac_restore_state file =
 (************)
 (* Commands *)
 
-let vernac_declare_tactic_definition (local,x,def) =
+let vernac_declare_tactic_definition locality (x,def) =
+  let local = make_module_locality locality in
   Tacintern.add_tacdef local x def
 
-let vernac_create_hintdb local id b =
+let vernac_create_hintdb locality id b =
+  let local = make_module_locality locality in
   Auto.create_hint_db local id full_transparent_state b
 
-let vernac_remove_hints local dbs ids =
+let vernac_remove_hints locality dbs ids =
+  let local = make_module_locality locality in
   Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
 
-let vernac_hints local lb h =
+let vernac_hints locality local lb h =
+  let local = enforce_module_locality locality local in
   Auto.add_hints local lb (Auto.interp_hints h)
 
-let vernac_syntactic_definition lid =
+let vernac_syntactic_definition locality lid x local y =
   Dumpglob.dump_definition lid false "syndef";
-  Metasyntax.add_syntactic_definition (snd lid)
+  let local = enforce_module_locality locality local in
+  Metasyntax.add_syntactic_definition (snd lid) x local y
 
-let vernac_declare_implicits local r = function
+let vernac_declare_implicits locality r l =
+  let local = make_section_locality locality in
+  match l with
   | [] ->
       Impargs.declare_implicits local (smart_global r)
   | _::_ as imps ->
       Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
-let vernac_declare_arguments local r l nargs flags =
+let vernac_declare_arguments locality r l nargs flags =
   let extra_scope_flag = List.mem `ExtraScopes flags in
   let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
   let names, rest = List.hd names, List.tl names in
@@ -989,7 +1015,9 @@ let vernac_declare_arguments local r l nargs flags =
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
       error "To rename arguments the \"rename\" flag must be specified."
-    else Arguments_renaming.rename_arguments local sr names_decl;
+    else
+      Arguments_renaming.rename_arguments
+        (make_section_locality locality) sr names_decl;
   (* All other infos are in the first item of l *)
   let l = List.hd l in
   let some_implicits_specified = match implicits with
@@ -1006,11 +1034,11 @@ let vernac_declare_arguments local r l nargs flags =
     Util.List.map_filter (function (n, true) -> Some n | _ -> None)
       (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
   if some_scopes_specified || List.mem `ClearScopes flags then
-    vernac_arguments_scope local r scopes;
+    vernac_arguments_scope locality r scopes;
   if not some_implicits_specified && List.mem `DefaultImplicits flags then
-    vernac_declare_implicits local r []
+    vernac_declare_implicits locality r []
   else if some_implicits_specified || List.mem `ClearImplicits flags then
-    vernac_declare_implicits local r implicits;
+    vernac_declare_implicits locality r implicits;
   if nargs >= 0 && nargs < List.fold_left max 0 rargs then
     error "The \"/\" option must be placed after the last \"!\".";
   let rec narrow = function
@@ -1020,7 +1048,8 @@ let vernac_declare_arguments local r l nargs flags =
   if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then
     match sr with
     | ConstRef _ as c ->
-       Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
+       Tacred.set_simpl_behaviour
+         (make_section_locality locality) c (rargs, nargs, flags)
     | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
 
 let vernac_reserve bl =
@@ -1031,7 +1060,9 @@ let vernac_reserve bl =
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
 
-let vernac_generalizable = Implicit_quantifiers.declare_generalizable
+let vernac_generalizable locality =
+  let local = make_non_locality locality in
+  Implicit_quantifiers.declare_generalizable local
 
 let _ =
   declare_bool_option
@@ -1284,15 +1315,27 @@ let _ =
       optread  = (fun () -> !Constrintern.parsing_explicit);
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
-let vernac_set_opacity local str =
+let vernac_set_strategy locality l =
+  let local = make_locality locality in
   let glob_ref r =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
       | _ -> error
           "cannot set an inductive type or a constructor as transparent" in
-  let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in
-  Redexpr.set_strategy local str
+  let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
+  Redexpr.set_strategy local l
+
+let vernac_set_opacity locality (v,l) =
+  let local = make_non_locality locality in
+  let glob_ref r =
+    match smart_global r with
+      | ConstRef sp -> EvalConstRef sp
+      | VarRef id -> EvalVarRef id
+      | _ -> error
+          "cannot set an inductive type or a constructor as transparent" in
+  let l = List.map glob_ref l in
+  Redexpr.set_strategy local [v,l]
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
@@ -1356,7 +1399,8 @@ let vernac_check_may_eval redexp glopt rc =
 	msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
-  declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r))
+  let local = make_locality locality in
+  declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
@@ -1670,30 +1714,36 @@ let vernac_check_guard () =
   in
   msg_notice message
 
-let interp c = match c with
+(* "locality" is the prefix "Local" attribute, while the "local" component
+ * is the outdated/deprecated "Local" attribute of some vernacular commands
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility *)
+let interp locality c = match c with
   (* Control (done in vernac) *)
   | (VernacTime _|VernacList _|VernacLoad _|VernacTimeout _|VernacFail _) ->
       assert false
 
   (* Syntax *)
-  | VernacTacticNotation (b,n,r,e) -> Metasyntax.add_tactic_notation (b,n,r,e)
-  | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
+  | VernacTacticNotation (n,r,e) ->
+      Metasyntax.add_tactic_notation (make_module_locality locality,n,r,e)
+  | VernacSyntaxExtension (local,sl) ->
+      vernac_syntax_extension locality local sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
-  | VernacOpenCloseScope sc -> vernac_open_close_scope sc
-  | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl
-  | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
-  | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
+  | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s
+  | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope locality qid scl
+  | VernacInfix (local,mv,qid,sc) -> vernac_infix locality local mv qid sc
+  | VernacNotation (local,c,infpl,sc) ->
+      vernac_notation locality local c infpl sc
 
   (* Gallina *)
-  | VernacDefinition (k,lid,d) -> vernac_definition k lid d
+  | VernacDefinition (k,lid,d) -> vernac_definition locality k lid d
   | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
-  | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
+  | VernacAssumption (stre,nl,l) -> vernac_assumption locality stre l nl
   | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
-  | VernacFixpoint (local, l) -> vernac_fixpoint local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint local l
+  | VernacFixpoint (local, l) -> vernac_fixpoint locality local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
 
@@ -1714,14 +1764,15 @@ let interp c = match c with
   | VernacRequire (export, qidl) -> vernac_require export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
-  | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t
-  | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
+  | VernacCoercion (local,r,s,t) -> vernac_coercion locality local r s t
+  | VernacIdentityCoercion (local,(_,id),s,t) ->
+      vernac_identity_coercion locality local id s t
 
   (* Type classes *)
-  | VernacInstance (abst, glob, sup, inst, props, pri) ->
-      vernac_instance abst glob sup inst props pri
+  | VernacInstance (abst, sup, inst, props, pri) ->
+      vernac_instance abst locality sup inst props pri
   | VernacContext sup -> vernac_context sup
-  | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids
+  | VernacDeclareInstances ids -> vernac_declare_instances locality ids
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
@@ -1733,7 +1784,7 @@ let interp c = match c with
   | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
   | VernacRemoveLoadPath s -> vernac_remove_loadpath s
   | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s
-  | VernacDeclareMLModule (local, l) -> vernac_declare_ml_module local l
+  | VernacDeclareMLModule l -> vernac_declare_ml_module locality l
   | VernacChdir s -> vernac_chdir s
 
   (* State management *)
@@ -1747,24 +1798,30 @@ let interp c = match c with
   | VernacBackTo n -> vernac_backto n
 
   (* Commands *)
-  | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def
-  | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
-  | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids
-  | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
-  | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
-  | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags 
+  | VernacDeclareTacticDefinition def ->
+      vernac_declare_tactic_definition locality def
+  | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b
+  | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids
+  | VernacHints (local,dbnames,hints) ->
+      vernac_hints locality local dbnames hints
+  | VernacSyntacticDefinition (id,c,local,b) ->
+      vernac_syntactic_definition locality  id c local b
+  | VernacDeclareImplicits (qid,l) ->
+      vernac_declare_implicits locality qid l
+  | VernacArguments (qid, l, narg, flags) ->
+      vernac_declare_arguments locality qid l narg flags 
   | VernacReserve bl -> vernac_reserve bl
-  | VernacGeneralizable (local,gen) -> vernac_generalizable local gen
-  | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
-  | VernacSetOption (locality,key,v) -> vernac_set_option locality key v
-  | VernacUnsetOption (locality,key) -> vernac_unset_option locality key
+  | VernacGeneralizable gen -> vernac_generalizable locality gen
+  | VernacSetOpacity qidl -> vernac_set_opacity locality qidl
+  | VernacSetStrategy l -> vernac_set_strategy locality l
+  | VernacSetOption (key,v) -> vernac_set_option locality key v
+  | VernacUnsetOption key -> vernac_unset_option locality key
   | VernacRemoveOption (key,v) -> vernac_remove_option key v
   | VernacAddOption (key,v) -> vernac_add_option key v
   | VernacMemOption (key,v) -> vernac_mem_option key v
   | VernacPrintOption key -> vernac_print_option key
   | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c
-  | VernacDeclareReduction (b,s,r) -> vernac_declare_reduction b s r
+  | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
   | VernacPrint p -> vernac_print p
   | VernacSearch (s,r) -> vernac_search s r
@@ -1798,23 +1855,58 @@ let interp c = match c with
   | VernacToplevelControl e -> raise e
 
   (* Extensions *)
-  | VernacExtend (opn,args) -> Vernacinterp.call (opn,args)
+  | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args)
+
+  (* Handled elsewhere *)
+  | VernacProgram _
+  | VernacLocal _ -> assert false
+
+(* Vernaculars that take a locality flag *)
+let check_vernac_supports_locality c l =
+  match l, c with
+  | None, _ -> ()
+  | Some _, (
+      VernacTacticNotation _
+    | VernacOpenCloseScope _
+    | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+    | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
+    | VernacAssumption _
+    | VernacCoercion _ | VernacIdentityCoercion _
+    | VernacInstance _ | VernacDeclareInstances _
+    | VernacDeclareMLModule _
+    | VernacDeclareTacticDefinition _
+    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+    | VernacSyntacticDefinition _
+    | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
+    | VernacGeneralizable _
+    | VernacSetOpacity _ | VernacSetStrategy _
+    | VernacSetOption _ | VernacUnsetOption _
+    | VernacDeclareReduction _
+    | VernacExtend _ ) -> ()
+  | Some _, _ -> Errors.error "This command does not support Locality"
 
 let interp c =
-  let mode = Flags.is_program_mode () in
-  let isprogcmd = !Flags.program_cmd in
-  Flags.program_cmd := false;
-  Obligations.set_program_mode isprogcmd;
-  try
-    interp c; Locality.check_locality ();
-    if not (not mode && !Flags.program_mode && not isprogcmd) then
-      Flags.program_mode := mode;
-    true
-  with
-    | UnsafeSuccess ->
-      Flags.program_mode := mode;
-      false
-    | reraise ->
-      let e = Errors.push reraise in
-      Flags.program_mode := mode;
-      raise e
+  let orig_program_mode = Flags.is_program_mode () in
+  let rec aux ?locality isprogcmd = function
+    | VernacProgram c when not isprogcmd -> aux ?locality true c
+    | VernacProgram _ -> Errors.error "Program mode specified twice"
+    | VernacLocal (b, c) when locality = None -> aux ~locality:b isprogcmd c
+    | VernacLocal _ -> Errors.error "Locality specified twice"
+    | c -> 
+        check_vernac_supports_locality c locality;
+        Obligations.set_program_mode isprogcmd;
+        try
+          interp locality c;
+          if orig_program_mode || not !Flags.program_mode || isprogcmd then
+            Flags.program_mode := orig_program_mode;
+          true
+        with
+          | UnsafeSuccess ->
+            Flags.program_mode := orig_program_mode;
+            false
+          | reraise ->
+            let e = Errors.push reraise in
+            Flags.program_mode := orig_program_mode;
+            raise e
+  in
+    aux false c
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index e15edf4e9a..2cc33dadc7 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -40,14 +40,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab
 
 (* Interpretation of a vernac command *)
 
-let call (opn,converted_args) =
+let call ?locality (opn,converted_args) =
   let loc = ref "Looking up command" in
   try
     let callback = vinterp_map opn in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
     loc:= "Executing command";
-    hunk()
+    Locality.LocalityFixme.set locality;
+    hunk();
+    Locality.LocalityFixme.assert_consumed()
   with
     | Drop -> raise Drop
     | reraise ->
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 7138c36f1e..4c2b66ed88 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -15,4 +15,4 @@ val overwriting_vinterp_add :
   string -> (raw_generic_argument list -> unit -> unit) -> unit
 
 val vinterp_init : unit -> unit
-val call : string * raw_generic_argument list -> unit
+val call : ?locality:bool -> string * raw_generic_argument list -> unit