Merge PR #1049: Remove obsolete locality

3 files changed, 69 insertions, 93 deletions

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 7e01d97cc..63f358a9d 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) ->