Remove "obsolete_locality" and fix STM vernac classification.

We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.

We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.

This is a preliminary step for the work on attributes.

16 files changed, 202 insertions, 277 deletions

diff --git a/API/API.mli b/API/API.mli
index 1a84600ec..321a0b808 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1302,6 +1302,10 @@ sig
     | CoFinite
     | BiFinite
 
+  type discharge =
+    | DoDischarge
+    | NoDischarge
+
   type locality =
     | Discharge
     | Local
@@ -1320,6 +1324,7 @@ sig
     | IdentityCoercion
     | Instance
     | Method
+    | Let
   type theorem_kind =
     | Theorem
     | Lemma
@@ -4028,8 +4033,6 @@ sig
 
   type verbose_flag = bool
 
-  type obsolete_locality = bool
-
   type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl
 
   type ident_decl = lident * universe_decl_expr option
@@ -4144,29 +4147,27 @@ sig
   | VernacRedirect of string * vernac_expr Loc.located
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
-  | VernacSyntaxExtension of
-      bool * obsolete_locality * (lstring * syntax_modifier list)
-  | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
+  | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
+  | VernacOpenCloseScope of bool * scope_name
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
+  | VernacInfix of (lstring * syntax_modifier list) *
       Constrexpr.constr_expr * scope_name option
   | VernacNotation of
-      obsolete_locality * Constrexpr.constr_expr * (lstring * syntax_modifier list) *
+      Constrexpr.constr_expr * (lstring * syntax_modifier list) *
       scope_name option
   | VernacNotationAddFormat of string * string * string
-  | VernacDefinition of
-      (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr
+  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * ident_decl * definition_expr
   | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of Constrexpr.constr_expr
-  | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
+  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
       inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list
   | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
-      Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
+      Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-      Decl_kinds.locality option * (cofixpoint_expr * decl_notation list) list
+      Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
@@ -4177,9 +4178,9 @@ sig
       Libnames.reference option * bool option * Libnames.reference list
   | VernacImport of bool * Libnames.reference list
   | VernacCanonical of Libnames.reference Misctypes.or_by_notation
-  | VernacCoercion of obsolete_locality * Libnames.reference Misctypes.or_by_notation *
+  | VernacCoercion of Libnames.reference Misctypes.or_by_notation *
       class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of obsolete_locality * lident *
+  | VernacIdentityCoercion of lident *
       class_rawexpr * class_rawexpr
   | VernacNameSectionHypSet of lident * section_subset_expr
   | VernacInstance of
@@ -4213,9 +4214,9 @@ sig
   | VernacBackTo of int
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * Libnames.reference list
-  | VernacHints of obsolete_locality * string list * hints_expr
+  | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) *
-      obsolete_locality * onlyparsing_flag
+      onlyparsing_flag
   | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation *
                                 (Constrexpr.explicitation * bool * bool) list list
   | VernacArguments of Libnames.reference Misctypes.or_by_notation *
diff --git a/CHANGES b/CHANGES
index 7a326c589..6a7a5a42b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,6 +21,10 @@ Tactics
 - Tactic "decide equality" now able to manage constructors which
   contain proofs.
 
+Vernacular Commands
+- The deprecated Coercion Local, Open Local Scope, Notation Local syntax
+  was removed. Use Local as a prefix instead.
+
 Changes from 8.7+beta2 to 8.7.0
 ===============================
 
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 13ed65056..0197cf9ae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -72,7 +72,7 @@ open Decl_kinds
 let type_of_logical_kind = function
   | IsDefinition def ->
       (match def with
-      | Definition -> "def"
+      | Definition | Let -> "def"
       | Coercion -> "coe"
       | SubClass -> "subclass"
       | CanonicalStructure -> "canonstruc"
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index a97758833..1dea6d9e9 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -8,6 +8,8 @@
 
 (** Informal mathematical status of declarations *)
 
+type discharge = DoDischarge | NoDischarge
+
 type locality = Discharge | Local | Global
 
 type binding_kind = Explicit | Implicit
@@ -40,6 +42,7 @@ type definition_object_kind =
   | IdentityCoercion
   | Instance
   | Method
+  | Let
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 96bcba5e8..5c9141fd6 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -151,10 +151,6 @@ type onlyparsing_flag = Flags.compat_version option
     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 = Goptions.option_value =
   | BoolValue of bool
@@ -327,31 +323,27 @@ type vernac_expr =
   | VernacFail of vernac_expr
 
   (* Syntax *)
-  | VernacSyntaxExtension of
-      bool * obsolete_locality * (lstring * syntax_modifier list)
-  | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
+  | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
+  | VernacOpenCloseScope of bool * scope_name
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
+  | VernacInfix of (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of
-      obsolete_locality * constr_expr * (lstring * syntax_modifier list) *
+      constr_expr * (lstring * syntax_modifier list) *
       scope_name option
   | VernacNotationAddFormat of string * string * string
 
   (* Gallina *)
-  | VernacDefinition of
-      (locality option * definition_object_kind) * ident_decl * definition_expr
+  | VernacDefinition of (discharge * definition_object_kind) * ident_decl * definition_expr
   | VernacStartTheoremProof of theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of (locality option * assumption_object_kind) *
+  | VernacAssumption of (discharge * assumption_object_kind) *
       inline * (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_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
+  | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
@@ -364,10 +356,9 @@ type vernac_expr =
       reference option * export_flag option * reference list
   | VernacImport of export_flag * reference list
   | VernacCanonical of reference or_by_notation
-  | VernacCoercion of obsolete_locality * reference or_by_notation *
-      class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of obsolete_locality * lident *
+  | VernacCoercion of reference or_by_notation *
       class_rawexpr * class_rawexpr
+  | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
   | VernacNameSectionHypSet of lident * section_subset_expr 
 
   (* Type classes *)
@@ -418,9 +409,9 @@ type vernac_expr =
   (* Commands *)
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
-  | VernacHints of obsolete_locality * string list * hints_expr
+  | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
-      obsolete_locality * onlyparsing_flag
+      onlyparsing_flag
   | VernacDeclareImplicits of reference or_by_notation *
       (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
diff --git a/library/kindops.ml b/library/kindops.ml
index 882f62086..83985ce97 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -23,45 +23,13 @@ let string_of_theorem_kind = function
   | Proposition -> "Proposition"
   | Corollary -> "Corollary"
 
-let string_of_definition_kind def =
-  let (locality, poly, kind) = def in
-  let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in
-  match kind with
-  | Definition ->
-    begin match locality with
-    | Discharge -> "Let"
-    | Local -> "Local Definition"
-    | Global -> "Definition"
-    end
-  | Example ->
-    begin match locality with
-    | Discharge -> error ()
-    | Local -> "Local Example"
-    | Global -> "Example"
-    end
-  | Coercion ->
-    begin match locality with
-    | Discharge -> error ()
-    | Local -> "Local Coercion"
-    | Global -> "Coercion"
-    end
-  | SubClass ->
-    begin match locality with
-    | Discharge -> error ()
-    | Local -> "Local SubClass"
-    | Global -> "SubClass"
-    end
-  | CanonicalStructure ->
-    begin match locality with
-    | Discharge -> error ()
-    | Local -> error ()
-    | Global -> "Canonical Structure"
-    end
-  | Instance ->
-    begin match locality with
-    | Discharge -> error ()
-    | Local -> "Instance"
-    | Global -> "Global Instance"
-    end
+let string_of_definition_object_kind = function
+  | Definition -> "Definition"
+  | Example -> "Example"
+  | Coercion -> "Coercion"
+  | SubClass -> "SubClass"
+  | CanonicalStructure -> "Canonical Structure"
+  | Instance -> "Instance"
+  | Let -> "Let"
   | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
     CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/kindops.mli b/library/kindops.mli
index 77979c915..06f873e85 100644
--- a/library/kindops.mli
+++ b/library/kindops.mli
@@ -12,4 +12,4 @@ open Decl_kinds
 
 val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_kind : definition_kind -> string
+val string_of_definition_object_kind : definition_object_kind -> string
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f10d74677..d88f6fa0d 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -70,19 +70,16 @@ GEXTEND Gram
 	    VernacCreateHintDb (id, b)
       | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
 	  VernacRemoveHints (dbnames, ids)
-      | IDENT "Hint"; local = obsolete_locality; h = hint;
+      | IDENT "Hint"; h = hint;
 	  dbnames = opt_hintbases ->
-	  VernacHints (local,dbnames, h)
+          VernacHints (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; 
 	info = hint_info; dbnames = opt_hintbases ->
-	  VernacHints (false,dbnames,
+          VernacHints (dbnames,
 	    HintsResolve (List.map (fun x -> (info, true, x)) lc))
       ] ];
-  obsolete_locality:
-    [ [ IDENT "Local" -> true | -> false ] ]
-  ;
   reference_or_constr:
    [ [ r = global -> HintsReference r
      | c = constr -> HintsConstr c ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0e585cff7..444f36833 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -149,7 +149,7 @@ GEXTEND Gram
       | d = def_token; id = ident_decl; b = def_body ->
           VernacDefinition (d, id, b)
       | IDENT "Let"; id = identref; b = def_body ->
-          VernacDefinition ((Some Discharge, Definition), (id, None), b)
+          VernacDefinition ((DoDischarge, Let), (id, None), b)
       (* Gallina inductive declarations *)
       | cum = cumulativity_token; priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -167,13 +167,13 @@ GEXTEND Gram
 	  in
           VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (None, recs)
+          VernacFixpoint (NoDischarge, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (Some Discharge, recs)
+          VernacFixpoint (DoDischarge, recs)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (None, corecs)
+          VernacCoFixpoint (NoDischarge, corecs)
       | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (Some Discharge, corecs)
+          VernacCoFixpoint (DoDischarge, 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)
@@ -195,23 +195,23 @@ GEXTEND Gram
       | IDENT "Property" -> Property ] ]
   ;
   def_token:
-    [ [ "Definition" -> (None, Definition)
-      | IDENT "Example" -> (None, Example)
-      | IDENT "SubClass" -> (None, SubClass) ] ]
+    [ [ "Definition" -> (NoDischarge,Definition)
+      | IDENT "Example" -> (NoDischarge,Example)
+      | IDENT "SubClass" -> (NoDischarge,SubClass) ] ]
   ;
   assumption_token:
-    [ [ "Hypothesis" -> (Some Discharge, Logical)
-      | "Variable" -> (Some Discharge, Definitional)
-      | "Axiom" -> (None, Logical)
-      | "Parameter" -> (None, Definitional)
-      | IDENT "Conjecture" -> (None, Conjectural) ] ]
+    [ [ "Hypothesis" -> (DoDischarge, Logical)
+      | "Variable" -> (DoDischarge, Definitional)
+      | "Axiom" -> (NoDischarge, Logical)
+      | "Parameter" -> (NoDischarge, Definitional)
+      | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ]
   ;
   assumptions_token:
-    [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical))
-      | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional))
-      | IDENT "Axioms" -> ("Axioms", (None, Logical))
-      | IDENT "Parameters" -> ("Parameters", (None, Definitional))
-      | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ]
+    [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical))
+      | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional))
+      | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical))
+      | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional))
+      | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
@@ -620,34 +620,22 @@ GEXTEND Gram
       | IDENT "Canonical"; IDENT "Structure"; qid = global;
           d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition
-	    ((Some Global,CanonicalStructure),((Loc.tag s),None),d)
+          VernacLocal(false,
+          VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d))
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((None,Coercion),((Loc.tag s),None),d)
-      | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
-           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.tag s),None),d)
-      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
-         ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
-	   VernacIdentityCoercion (true, f, s, t)
+          VernacDefinition ((NoDischarge,Coercion),((Loc.tag s),None),d)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
-	   VernacIdentityCoercion (false, f, s, t)
-      | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
-	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (true, AN qid, s, t)
-      | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":";
-	 s = class_rawexpr; ">->"; t = class_rawexpr ->
-	  VernacCoercion (true, ByNotation ntn, s, t)
+           VernacIdentityCoercion (f, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (false, AN qid, s, t)
+          VernacCoercion (AN qid, s, t)
       | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (false, ByNotation ntn, s, t)
+          VernacCoercion (ByNotation ntn, s, t)
 
       | IDENT "Context"; c = binders ->
 	  VernacContext c
@@ -1106,11 +1094,11 @@ GEXTEND Gram
   GLOBAL: syntax;
 
   syntax:
-   [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (local,(true,sc))
+   [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
+         VernacOpenCloseScope (true,sc)
 
-     | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT ->
-         VernacOpenCloseScope (local,(false,sc))
+     | IDENT "Close"; IDENT "Scope"; sc = IDENT ->
+         VernacOpenCloseScope (false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc, Some key)
@@ -1120,32 +1108,31 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Infix"; local = obsolete_locality;
-	 op = ne_lstring; ":="; p = constr;
+     | IDENT "Infix"; op = ne_lstring; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (local,(op,modl),p,sc)
-     | IDENT "Notation"; local = obsolete_locality; id = identref;
+         VernacInfix ((op,modl),p,sc)
+     | IDENT "Notation"; id = identref;
 	 idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            VernacSyntacticDefinition
-	     (id,(idl,c),local,b)
-     | IDENT "Notation"; local = obsolete_locality; s = lstring; ":=";
+             (id,(idl,c),b)
+     | IDENT "Notation"; s = lstring; ":=";
 	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,c,(s,modl),sc)
+           VernacNotation (c,(s,modl),sc)
      | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING ->
            VernacNotationAddFormat (n,s,fmt)
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
 	   let (loc,s) = s in
-	   VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l))
+           VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l))
 
-     | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
+     | IDENT "Reserved"; IDENT "Notation";
 	 s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (false, local,(s,l))
+         -> VernacSyntaxExtension (false, (s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order
         to factorize with other "Print"-based vernac entries *)
@@ -1158,9 +1145,6 @@ GEXTEND Gram
          Some (parse_compat_version s)
       | -> None ] ]
   ;
-  obsolete_locality:
-    [ [ IDENT "Local" -> true | -> false ] ]
-  ;
   level:
     [ [ IDENT "level"; n = natural -> NumLevel n
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 829556a71..87609296b 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+             (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7385ed84c..3efb7b914 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -551,9 +551,9 @@ GEXTEND Gram
       | IDENT "Canonical"; qid = Constr.global;
           d = G_vernac.def_body ->
           let s = coerce_reference_to_id qid in
-	  Vernacexpr.VernacDefinition
-	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
-             ((Loc.tag s),None),(d  ))
+    Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition
+      ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
+          ((Loc.tag s),None),(d  )))
   ]];
 END
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 1a74538aa..46ef2ac03 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -324,23 +324,18 @@ open Decl_kinds
     | SortClass -> keyword "Sortclass"
     | RefClass qid -> pr_smart_global qid
 
-  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) ->
-        keyword (if many then "Hypotheses" else "Hypothesis")
-      | (Discharge,Definitional) ->
-        keyword (if many then "Variables" else "Variable")
-      | (Global,Logical) ->
+  let pr_assumption_token many discharge kind =
+    match discharge, kind with
+      | (NoDischarge,Logical) ->
         keyword (if many then "Axioms" else "Axiom")
-      | (Global,Definitional) ->
+      | (NoDischarge,Definitional) ->
         keyword (if many then "Parameters" else "Parameter")
-      | (Local, Logical) ->
-        keyword (if many then "Local Axioms" else "Local Axiom")
-      | (Local,Definitional) ->
-        keyword (if many then "Local Parameters" else "Local Parameter")
-      | (Global,Conjectural) -> str"Conjecture"
-      | ((Discharge | Local),Conjectural) ->
+      | (NoDischarge,Conjectural) -> str"Conjecture"
+      | (DoDischarge,Logical) ->
+        keyword (if many then "Hypotheses" else "Hypothesis")
+      | (DoDischarge,Definitional) ->
+        keyword (if many then "Variables" else "Variable")
+      | (DoDischarge,Conjectural) ->
         anomaly (Pp.str "Don't know how to beautify a local conjecture.")
 
   let pr_params pr_c (xl,(c,t)) =
@@ -631,7 +626,7 @@ open Decl_kinds
         return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
 
     (* Syntax *)
-      | VernacOpenCloseScope (_,(opening,sc)) ->
+      | VernacOpenCloseScope (opening,sc) ->
         return (
           keyword (if opening then "Open " else "Close ") ++
             keyword "Scope" ++ spc() ++ str sc
@@ -660,7 +655,7 @@ open Decl_kinds
           ++ spc() ++ pr_smart_global q
           ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
         )
-      | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *)
+      | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *)
         return (
           hov 0 (hov 0 (keyword "Infix "
                         ++ qs s ++ str " :=" ++ pr_constrarg q) ++
@@ -669,7 +664,7 @@ open Decl_kinds
                      | None -> mt()
                      | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
         )
-      | VernacNotation (_,c,((_,s),l),opt) ->
+      | VernacNotation (c,((_,s),l),opt) ->
         return (
           hov 2 (keyword "Notation" ++ spc() ++ qs s ++
                    str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
@@ -677,7 +672,7 @@ open Decl_kinds
                      | None -> mt()
                      | Some sc -> str" :" ++ spc() ++ str sc))
         )
-      | VernacSyntaxExtension (_, _,(s,l)) ->
+      | VernacSyntaxExtension (_, (s, l)) ->
         return (
           keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++
             pr_syntax_modifiers l
@@ -688,10 +683,9 @@ open Decl_kinds
         )
 
       (* Gallina *)
-      | VernacDefinition (d,id,b) -> (* A verifier... *)
-        let pr_def_token (l,dk) =
-          let l = match l with Some x -> x | None -> Decl_kinds.Global in
-          keyword (Kindops.string_of_definition_kind (l,false,dk))
+      | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *)
+        let pr_def_token dk =
+          keyword (Kindops.string_of_definition_object_kind dk)
         in
         let pr_reduce = function
           | None -> mt()
@@ -712,7 +706,7 @@ open Decl_kinds
         let (binds,typ,c) = pr_def_body b in
         return (
           hov 2 (
-            pr_def_token d ++ spc()
+            pr_def_token kind ++ spc()
             ++ pr_ident_decl id ++ binds ++ typ
             ++ (match c with
               | None -> mt()
@@ -737,13 +731,13 @@ open Decl_kinds
       )
       | VernacExactProof c ->
         return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
-      | VernacAssumption (stre,t,l) ->
+      | VernacAssumption ((discharge,kind),t,l) ->
         let n = List.length (List.flatten (List.map fst (List.map snd l))) in
         let pr_params (c, (xl, t)) =
           hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++
             (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in
         let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
-        return (hov 2 (pr_assumption_token (n > 1) stre ++
+        return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
                        pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
       | VernacInductive (cum, p,f,l) ->
         let pr_constructor (coe,(id,c)) =
@@ -793,9 +787,8 @@ open Decl_kinds
 
       | VernacFixpoint (local, recs) ->
         let local = match local with
-          | Some Discharge -> "Let "
-          | Some Local -> "Local "
-          | None | Some Global -> ""
+          | DoDischarge -> "Let "
+          | NoDischarge -> ""
         in
         return (
           hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
@@ -805,9 +798,8 @@ open Decl_kinds
 
       | VernacCoFixpoint (local, corecs) ->
         let local = match local with
-          | Some Discharge -> keyword "Let" ++ spc ()
-          | Some Local -> keyword "Local" ++ spc ()
-          | None | Some Global -> str ""
+          | DoDischarge -> keyword "Let" ++ spc ()
+          | NoDischarge -> str ""
         in
         let pr_onecorec ((iddecl,bl,c,def),ntn) =
           pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -868,14 +860,14 @@ open Decl_kinds
         return (
           keyword "Canonical Structure" ++ spc() ++ pr_smart_global q
         )
-      | VernacCoercion (_,id,c1,c2) ->
+      | VernacCoercion (id,c1,c2) ->
         return (
           hov 1 (
             keyword "Coercion" ++ spc() ++
               pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++
               spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2)
         )
-      | VernacIdentityCoercion (_,id,c1,c2) ->
+      | VernacIdentityCoercion (id,c1,c2) ->
         return (
           hov 1 (
             keyword "Identity Coercion" ++ spc() ++ pr_lident id ++
@@ -999,9 +991,9 @@ open Decl_kinds
                    prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++
                    pr_opt_hintbases dbnames)
         )
-      | VernacHints (_, dbnames,h) ->
+      | VernacHints (dbnames,h) ->
         return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
-      | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
+      | VernacSyntacticDefinition (id,(ids,c),compat) ->
         return (
           hov 2
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3aa2cd707..1ca572a36 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -103,8 +103,7 @@ let rec classify_vernac e =
     | VernacUnsetOption (["Default";"Proof";"Using"])
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
     (* StartProof *)
-    | VernacDefinition (
-       (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
+    | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
@@ -113,19 +112,29 @@ let rec classify_vernac e =
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
         VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
     | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
-    | VernacFixpoint (_,l) ->
+    | VernacFixpoint (discharge,l) ->
+       let guarantee =
+         match discharge with
+         | Decl_kinds.NoDischarge -> GuaranteesOpacity
+         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+       in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
         else VtSideff ids, VtLater
-    | VernacCoFixpoint (_,l) ->
+    | VernacCoFixpoint (discharge,l) ->
+       let guarantee =
+         match discharge with
+         | Decl_kinds.NoDischarge -> GuaranteesOpacity
+         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+       in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 681b1ab20..87b411625 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -6,36 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Decl_kinds
+
 (** * Managing locality *)
 
 let local_of_bool = function
-  | true -> Decl_kinds.Local
-  | false -> Decl_kinds.Global
-
-(** Extracting the locality flag *)
-
-(* Commands which supported an inlined Local flag *)
-
-let warn_deprecated_local_syntax =
-  CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated"
-         (fun () ->
-          Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.")
-
-let enforce_locality_full locality_flag local =
-  let local =
-    match locality_flag with
-    | Some false when local ->
-	CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.")
-    | Some true when local ->
-	CErrors.user_err Pp.(str "Use only prefix \"Local\".")
-    | None ->
-	if local then begin
-	    warn_deprecated_local_syntax ();
-	    Some true
-	end else
-	None
-    | Some b -> Some b in
-  local
+  | true -> Local
+  | false -> Global
+
 
 (** Positioning locality for commands supporting discharging and export
      outside of modules *)
@@ -48,15 +26,16 @@ let make_non_locality = function Some false -> false | _ -> true
 
 let make_locality = function Some true -> true | _ -> false
 
-let enforce_locality locality_flag local =
-   make_locality (enforce_locality_full locality_flag local)
+let enforce_locality_exp locality_flag discharge =
+  match locality_flag, discharge with
+  | Some b, NoDischarge -> local_of_bool b
+  | None, NoDischarge -> Global
+  | None, DoDischarge -> Discharge
+  | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
+  | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
 
-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 _ -> CErrors.user_err Pp.(str "Local non allowed in this case")
+let enforce_locality locality_flag =
+   make_locality locality_flag
 
 (* For commands whose default is to not discharge but to export:
    Global in sections forces discharge, Global not in section is the default;
@@ -65,8 +44,8 @@ let enforce_locality_exp locality_flag local =
 let make_section_locality =
   function Some b -> b | None -> Lib.sections_are_opened ()
 
-let enforce_section_locality locality_flag local =
-  make_section_locality (enforce_locality_full locality_flag local)
+let enforce_section_locality locality_flag =
+  make_section_locality locality_flag
 
 (** Positioning locality for commands supporting export but not discharge *)
 
@@ -83,5 +62,5 @@ let make_module_locality = function
   | Some true -> true
   | None -> false
 
-let enforce_module_locality locality_flag local =
-  make_module_locality (enforce_locality_full locality_flag local)
+let enforce_module_locality locality_flag =
+  make_module_locality locality_flag
diff --git a/vernac/locality.mli b/vernac/locality.mli
index bef66d8bc..922538b23 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -8,10 +8,6 @@
 
 (** * Managing locality *)
 
-(** Commands which supported an inlined Local flag *)
-
-val enforce_locality_full : bool option -> bool -> bool option
-
 (** * Positioning locality for commands supporting discharging and export
     outside of modules *)
 
@@ -22,16 +18,15 @@ val enforce_locality_full : bool option -> bool -> bool option
 
 val make_locality : bool option -> 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
+val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality
+val enforce_locality : bool option -> 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 enforce_section_locality : bool option -> bool -> bool
+val enforce_section_locality : bool option -> bool
 
 (** * Positioning locality for commands supporting export but not discharge *)
 
@@ -40,4 +35,4 @@ val enforce_section_locality : bool option -> bool -> bool
     Local in sections is the default, Local not in section forces non-export *)
 
 val make_module_locality : bool option -> bool
-val enforce_module_locality : bool option -> bool -> bool
+val enforce_module_locality : bool option -> bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f3410bc1..1d9cb65f1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -409,8 +409,8 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension atts local infix l =
-  let local = enforce_module_locality atts.locality local in
+let vernac_syntax_extension atts infix l =
+  let local = enforce_module_locality atts.locality in
   if infix then Metasyntax.check_infix_modifiers (snd l);
   Metasyntax.add_syntax_extension local l
 
@@ -421,20 +421,20 @@ let vernac_delimiters sc = function
 let vernac_bind_scope sc cll =
   Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
 
-let vernac_open_close_scope ~atts local (b,s) =
-  let local = enforce_section_locality atts.locality local in
+let vernac_open_close_scope ~atts (b,s) =
+  let local = enforce_section_locality atts.locality in
   Notation.open_close_scope (local,b,s)
 
 let vernac_arguments_scope ~atts r scl =
   let local = make_section_locality atts.locality in
   Notation.declare_arguments_scope local (smart_global r) scl
 
-let vernac_infix ~atts local =
-  let local = enforce_module_locality atts.locality local in
+let vernac_infix ~atts =
+  let local = enforce_module_locality atts.locality in
   Metasyntax.add_infix local (Global.env())
 
-let vernac_notation ~atts local =
-  let local = enforce_module_locality atts.locality local in
+let vernac_notation ~atts =
+  let local = enforce_module_locality atts.locality in
   Metasyntax.add_notation local (Global.env())
 
 (***********)
@@ -472,16 +472,16 @@ let vernac_definition_hook p = function
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook
 
-let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def =
-  let local = enforce_locality_exp atts.locality local in
-  let hook = vernac_definition_hook atts.polymorphic k in
+let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
+  let local = enforce_locality_exp atts.locality discharge in
+  let hook = vernac_definition_hook atts.polymorphic kind in
   let () = match local with
   | Discharge -> Dumpglob.dump_definition lid true "var"
   | Local | Global -> Dumpglob.dump_definition lid false "def"
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-          start_proof_and_print (local, atts.polymorphic, DefinitionBody k)
+          start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
 	    [Some (lid,pl), (bl,t)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
@@ -489,10 +489,10 @@ let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def =
           | Some r ->
             let sigma, env = Pfedit.get_current_context () in
             Some (snd (Hook.get f_interp_redexp env sigma r)) in
-        do_definition id (local, atts.polymorphic,k) pl bl red_option c typ_opt hook)
+        do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof ~atts kind l =
-  let local = enforce_locality_exp atts.locality None in
+  let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
@@ -511,8 +511,8 @@ let vernac_exact_proof c =
   save_proof (Vernacexpr.(Proved(Opaque,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_assumption ~atts (local, kind) l nl =
-  let local = enforce_locality_exp atts.locality local in
+let vernac_assumption ~atts discharge kind l nl =
+  let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
   let kind = local, atts.polymorphic, kind in
   List.iter (fun (is_coe,(idl,c)) ->
@@ -594,14 +594,14 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
 
-let vernac_fixpoint ~atts local l =
-  let local = enforce_locality_exp atts.locality local in
+let vernac_fixpoint ~atts discharge l =
+  let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_fixpoint local atts.polymorphic l
 
-let vernac_cofixpoint ~atts local l =
-  let local = enforce_locality_exp atts.locality local in
+let vernac_cofixpoint ~atts discharge l =
+  let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint local atts.polymorphic l
@@ -812,16 +812,16 @@ let vernac_require from import qidl =
 let vernac_canonical r =
   Recordops.declare_canonical_structure (smart_global r)
 
-let vernac_coercion ~atts local ref qids qidt =
-  let local = enforce_locality atts.locality local in
+let vernac_coercion ~atts ref qids qidt =
+  let local = enforce_locality atts.locality 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 atts.polymorphic ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
-let vernac_identity_coercion ~atts local id qids qidt =
-  let local = enforce_locality atts.locality local in
+let vernac_identity_coercion ~atts id qids qidt =
+  let local = enforce_locality atts.locality in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target
@@ -947,13 +947,13 @@ let vernac_remove_hints ~atts dbs ids =
   let local = make_module_locality atts.locality in
   Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
 
-let vernac_hints ~atts local lb h =
-  let local = enforce_module_locality atts.locality local in
+let vernac_hints ~atts lb h =
+  let local = enforce_module_locality atts.locality in
   Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
 
-let vernac_syntactic_definition ~atts lid x local y =
+let vernac_syntactic_definition ~atts lid x y =
   Dumpglob.dump_definition lid false "syndef";
-  let local = enforce_module_locality atts.locality local in
+  let local = enforce_module_locality atts.locality in
   Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
 
 let vernac_declare_implicits ~atts r l =
@@ -1958,27 +1958,29 @@ let interp ?proof ~atts ~st c =
   | VernacLocal _ -> assert false
 
   (* Syntax *)
-  | VernacSyntaxExtension (infix, local,sl) ->
-      vernac_syntax_extension atts local infix sl
+  | VernacSyntaxExtension (infix, sl) ->
+      vernac_syntax_extension atts infix sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
-  | VernacOpenCloseScope (local, s) -> vernac_open_close_scope ~atts local s
+  | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
-  | VernacInfix (local,mv,qid,sc) -> vernac_infix ~atts local mv qid sc
-  | VernacNotation (local,c,infpl,sc) ->
-      vernac_notation ~atts local c infpl sc
+  | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
+  | VernacNotation (c,infpl,sc) ->
+      vernac_notation ~atts c infpl sc
   | VernacNotationAddFormat(n,k,v) ->
       Metasyntax.add_notation_extra_printing_rule n k v
 
   (* Gallina *)
-  | VernacDefinition (k,lid,d) -> vernac_definition ~atts k lid d
+  | VernacDefinition ((discharge,kind),lid,d) ->
+      vernac_definition ~atts discharge kind lid d
   | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
-  | VernacAssumption (stre,nl,l) -> vernac_assumption ~atts stre l nl
+  | VernacAssumption ((discharge,kind),nl,l) ->
+      vernac_assumption ~atts discharge kind l nl
   | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint ~atts local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~atts local l
+  | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l
+  | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe ~atts l
@@ -2003,9 +2005,9 @@ let interp ?proof ~atts ~st c =
   | VernacRequire (from, export, qidl) -> vernac_require from export qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
-  | VernacCoercion (local,r,s,t) -> vernac_coercion ~atts local r s t
-  | VernacIdentityCoercion (local,(_,id),s,t) ->
-      vernac_identity_coercion ~atts local id s t
+  | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
+  | VernacIdentityCoercion ((_,id),s,t) ->
+      vernac_identity_coercion ~atts id s t
 
   (* Type classes *)
   | VernacInstance (abst, sup, inst, props, info) ->
@@ -2031,10 +2033,10 @@ let interp ?proof ~atts ~st c =
   (* Commands *)
   | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b
   | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids
-  | VernacHints (local,dbnames,hints) ->
-      vernac_hints ~atts local dbnames hints
-  | VernacSyntacticDefinition (id,c,local,b) ->
-      vernac_syntactic_definition ~atts id c local b
+  | VernacHints (dbnames,hints) ->
+      vernac_hints ~atts dbnames hints
+  | VernacSyntacticDefinition (id,c,b) ->
+      vernac_syntactic_definition ~atts id c b
   | VernacDeclareImplicits (qid,l) ->
       vernac_declare_implicits ~atts qid l
   | VernacArguments (qid, args, more_implicits, nargs, flags) ->