- Standardized prefix use of "Local"/"Global" modifiers as decided in

  late 2008 Coq WG.
- Updated Copyright file wrt JProver.



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

10 files changed, 133 insertions, 80 deletions

diff --git a/COPYRIGHT b/COPYRIGHT
index 2cbb6fbce8..7ed31f15d7 100644
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -20,12 +20,6 @@ parsing/search.ml)
 	Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
 	Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
 
-Coq includes a tactic Jp based on JProver, a theorem prover for
-first-order intuitionistic logic.  Jprover was originally implemented
-by Stephan Schmitt and then integrated into MetaPRL by Aleksey
-Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL
-and then integrated it into Coq.
-	
 The file CREDITS contains a list of past contributors
 The credits section in Reference Manual introduction details
 contributions.
@@ -38,4 +32,4 @@ The Coq development Team (march 2004)
 	Pierre Letouzey (Université Paris Sud)
 	Claude Marché (Université Paris Sud-INRIA)
 	Christine Paulin (Université Paris Sud)	
-	Clément Renard (INRIA)
\ No newline at end of file
+	Clément Renard (INRIA)
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index b4bae4235d..6877db179b 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -181,8 +181,8 @@ valid coercion paths are ignored; they are signaled by a warning.
 \end{enumerate}
 
 \begin{Variants}
-\item {\tt Coercion Local {\qualid} : {\class$_1$} >-> {\class$_2$}.}
-\comindex{Coercion Local}\\
+\item {\tt Local Coercion {\qualid} : {\class$_1$} >-> {\class$_2$}.}
+\comindex{Local Coercion}\\
   Declares the construction denoted by {\qualid} as a coercion local to
   the current section.
 
@@ -196,8 +196,8 @@ valid coercion paths are ignored; they are signaled by a warning.
   \texttt{Definition {\ident} : {\type} := {\term}}, and then
   declares {\ident} as a coercion between it source and its target. 
 
-\item {\tt Coercion Local {\ident} := {\term}}\comindex{Coercion Local}\\
-  This defines {\ident} just like \texttt{Local {\ident} :=
+\item {\tt Local Coercion {\ident} := {\term}}\comindex{Local Coercion}\\
+  This defines {\ident} just like \texttt{Let {\ident} :=
     {\term}}, and then declares {\ident} as a coercion between it
   source and its target.
 
@@ -263,7 +263,7 @@ coercion between {\class$_1$} and {\class$_2$}.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Identity Coercion Local {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
+\item {\tt Local Identity Coercion {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\
 Idem but locally to the current section.
 
 \item {\tt SubClass {\ident} := {\type}.} \\
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1294ee7c0b..502b42b837 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1150,15 +1150,15 @@ have to) be skipped in any expression involving an application of
 {\qualid}.
 
 \begin{Variants}
-\item {\tt Implicit Arguments Global {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Implicit Arguments Global}}
+\item {\tt Global Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\comindex{Global Implicit Arguments}}
 
 Tells to recompute the implicit arguments of {\qualid} after ending of
 the current section if any, enforcing the implicit arguments known
 from inside the section to be the ones declared by the command.
 
-\item {\tt Implicit Arguments Local {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Implicit Arguments Local}}
+\item {\tt Local Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\comindex{Local Implicit Arguments}}
 
 When in a module, tells not to activate the implicit arguments of
 {\qualid} declared by this commands to contexts that requires the
@@ -1210,14 +1210,14 @@ Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversibl
 and also~\ref{SetMaximalImplicitInsertion}).
 
 \begin{Variants}
-\item {\tt Implicit Arguments Global {\qualid}
-\comindex{Implicit Arguments Global}}
+\item {\tt Global Implicit Arguments {\qualid}
+\comindex{Global Implicit Arguments}}
 
 Tells to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
-\item {\tt Implicit Arguments Local {\qualid}
-\comindex{Implicit Arguments Local}}
+\item {\tt Local Implicit Arguments {\qualid}
+\comindex{Local Implicit Arguments}}
 
 When in a module, tells not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 967a8180ad..6ade546b07 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -445,13 +445,13 @@ Locate "'exists' _ , _".
 \begin{centerframe}
 \begin{tabular}{lcl}
 {\sentence} & ::= & 
-   \texttt{Notation} \zeroone{\tt Local} {\str} \texttt{:=} {\term} 
+   \zeroone{\tt Local} \texttt{Notation} {\str} \texttt{:=} {\term} 
    \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
-   \texttt{Infix} \zeroone{\tt Local} {\str} \texttt{:=} {\qualid} 
+   \zeroone{\tt Local} \texttt{Infix} {\str} \texttt{:=} {\qualid} 
    \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
-   \texttt{Reserved Notation} \zeroone{\tt Local} {\str}
+   \zeroone{\tt Local} \texttt{Reserved Notation} {\str}
    \zeroone{\modifiers} .\\
   & $|$ & {\tt Inductive}
    \nelist{{\inductivebody} \zeroone{\declnotation}}{with}{\tt .}\\
@@ -625,7 +625,7 @@ the underlying \verb="{ x }"=-free rule which is \verb="y & z"=).
 \paragraph{Persistence of notations}
 
 Notations do not survive the end of sections. They survive modules
-unless the command {\tt Notation Local} is used instead of {\tt
+unless the command {\tt Local Notation} is used instead of {\tt
 Notation}.
 
 \section[Interpretation scopes]{Interpretation scopes\index{Interpretation scopes}
@@ -693,9 +693,9 @@ exported to the modules that import the module where they occur.
 
 \begin{Variants}
 
-\item {\tt Open Local Scope} {\scope}.
+\item {\tt Local Open Scope} {\scope}.
 
-\item {\tt Close Local Scope} {\scope}.
+\item {\tt Local Close Scope} {\scope}.
 
 These variants are not exported to the modules that import the module
 where they occur, even if outside a section.
@@ -743,13 +743,13 @@ is interpreted in the scope stack extended by the scopes bound (if any)
 to these arguments.
 
 \begin{Variants}
-\item {\tt Arguments Scope Global} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
 
 This behaves like {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]} but survives when a section is closed instead
 of stopping working at section closing.
 
-\item {\tt Arguments Scope Local} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
 
 This is a synonym of {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]}: if in a section, the effect of the command
@@ -973,7 +973,7 @@ abbreviation but at the time it is used. Especially, abbreviations can
 be bound to terms with holes (i.e. with ``\_''). The general syntax
 for abbreviations is
 \begin{quote}
-\texttt{Notation} \zeroone{{\tt Local}} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
+\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} 
  \zeroone{{\tt (only parsing)}}~\verb=.=
 \end{quote}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d806adea53..9ed2e650c4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3680,13 +3680,14 @@ adding transparency hints that make the network more constrained
 (c.f. \ref{HintTransparency}).
 
 \begin{Variants}
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
   \ident$_1$ \ldots\ \ident$_n$
   
   This is used to declare a hint database that must not be exported to the other
   modules that require and import the current module. Inside a
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
+
 \end{Variants}
 
 The general
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 35f02237aa..d5053dc822 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -92,10 +92,10 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
       | IDENT "Create"; local = locality; IDENT "HintDb" ; 
 	  id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
-	    VernacCreateHintDb (local, id, b)
+	    VernacCreateHintDb (enforce_locality_of local, id, b)
       | IDENT "Hint"; local = locality; h = hint;
         dbnames = opt_hintbases ->
-	  VernacHints (local,dbnames, h)
+	  VernacHints (enforce_locality_of local,dbnames, h)
 	  
 
 (*This entry is not commented, only for debug*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index bcb2f7a576..57c2ef6774 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,7 +64,13 @@ let default_command_entry =
 let no_hook _ _ = ()
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
-  vernac:
+  vernac: FIRST
+    [ [ IDENT "Time"; locality; v = vernac_aux -> 
+          check_locality (); VernacTime v 
+      | locality; v = vernac_aux -> 
+	  check_locality (); 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         *)
     [ [ g = gallina; "." -> g 
@@ -74,12 +80,14 @@ GEXTEND Gram
       | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
     ] ]
   ;
-  vernac: FIRST
-    [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
-  ;
-  vernac: LAST  
+  vernac_aux: LAST  
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
+  locality:
+    [ [ IDENT "Local" -> locality_flag := Some true
+      | IDENT "Global" -> locality_flag := Some false
+      | -> locality_flag := None ] ]
+  ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
@@ -109,10 +117,7 @@ END
 GEXTEND Gram
   GLOBAL: locality non_locality;
   locality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ]
-  ;
-  non_locality:
-    [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ]
+    [ [ IDENT "Local" -> true | -> false ] ]
   ;
 END
 
@@ -196,9 +201,8 @@ GEXTEND Gram
 	no_hook, (Local, Flags.boxed_definitions(), Definition)
       | IDENT "Example" -> 
 	no_hook, (Global, Flags.boxed_definitions(), Example)
-      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, false, SubClass)
-      | IDENT "Local"; IDENT "SubClass"  ->
-          Class.add_subclass_hook, (Local, false, SubClass) ] ] 
+      | IDENT "SubClass"  ->
+          Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
@@ -463,16 +467,13 @@ GEXTEND Gram
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-        IDENT "Transparent"; b = non_locality; l = LIST1 global ->
-          VernacSetOpacity (b,[Conv_oracle.transparent,l])
-      | IDENT "Opaque"; b = non_locality; l = LIST1 global ->
-          VernacSetOpacity (b,[Conv_oracle.Opaque, l])
+        IDENT "Transparent"; l = LIST1 global ->
+          VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l])
+      | IDENT "Opaque"; l = LIST1 global ->
+          VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l])
       | IDENT "Strategy"; l =
           LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
-            VernacSetOpacity (false,l)
-      | IDENT "Local"; IDENT "Strategy"; l =
-          LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] ->
-            VernacSetOpacity (true,l)
+            VernacSetOpacity (use_locality (),l)
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical qid
@@ -485,28 +486,27 @@ GEXTEND Gram
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_global_to_id qid in
-	  VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_global_to_id qid in
-	  VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Local, f, s, t)
+	   VernacIdentityCoercion (enforce_locality_exp (), f, s, t)
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	   VernacIdentityCoercion (Global, f, s, t)
+	   VernacIdentityCoercion (use_locality_exp (), f, s, t)
       | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
 	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
-	  VernacCoercion (Local, qid, s, t)
+	  VernacCoercion (enforce_locality_exp (), qid, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-	  VernacCoercion (Global, qid, s, t)
+	  VernacCoercion (use_locality_exp (), qid, s, t)
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
 	    
-      | IDENT "Instance"; local = non_locality; name = identref; 
-	 sup = OPT binders_let; ":";
+      | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; 
 	 props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
@@ -519,17 +519,15 @@ GEXTEND Gram
 	     let (loc, id) = name in 
 	       (loc, Name id)
 	   in
-	     VernacInstance (not local, sup, (n, expl, t), props, pri)
+	     VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; 
-	   local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; 
-	   qid = global; 
+      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
 	   pos = OPT [ "["; l = LIST0 implicit_name; "]" -> 
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   VernacDeclareImplicits (local,qid,pos)
+	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
@@ -792,10 +790,10 @@ GEXTEND Gram
 
   syntax:
    [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
-         VernacOpenCloseScope (local,true,sc)
+         VernacOpenCloseScope (enforce_locality_of local,true,sc)
 
      | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> 
-         VernacOpenCloseScope (local,false,sc)
+         VernacOpenCloseScope (enforce_locality_of local,false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -803,22 +801,23 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; local = non_locality; qid = global;
-       "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl)
+     | IDENT "Arguments"; IDENT "Scope"; qid = global;
+       "["; scl = LIST0 opt_scope; "]" -> 
+	 VernacArgumentsScope (use_non_locality (),qid,scl)
 
      | IDENT "Infix"; local = locality;
 	 op = ne_string; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (local,(op,modl),p,sc)
+         VernacInfix (enforce_locality_of local,(op,modl),p,sc)
      | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; 
 	 ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
-           VernacSyntacticDefinition (id,(idl,c),local,b)
+           VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,c,(s,modl),sc)
+           VernacNotation (enforce_locality_of local,c,(s,modl),sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
@@ -826,7 +825,7 @@ GEXTEND Gram
 
      | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,(s,l))
+	 -> VernacSyntaxExtension (enforce_locality_of 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/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 13b5e13dd2..1ff53294e5 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -1,4 +1,4 @@
-(* A few tests to check Argument Scope Global command *)
+(* A few tests to check Global Argument Scope command *)
 
 Section A.
 Variable a : bool -> bool.
@@ -11,11 +11,11 @@ About b.
 About negb''.
 About negb'.
 About negb.
-Arguments Scope Global negb'' [ _ ].
-Arguments Scope Global negb' [ _ ].
-Arguments Scope Global negb [ _ ].
-Arguments Scope Global a [ _ ].
-Arguments Scope Global b [ _ ].
+Global Arguments Scope negb'' [ _ ].
+Global Arguments Scope negb' [ _ ].
+Global Arguments Scope negb [ _ ].
+Global Arguments Scope a [ _ ].
+Global Arguments Scope b [ _ ].
 About a.
 About b.
 About negb.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 63f85bc707..4bdd579a60 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -30,4 +30,4 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
 (* Check import of notations from within a section *)
 
 Notation "+1 x" := (S x) (at level 25, x at level 9).
-Section A. Notation Global "'Z'" := O (at level 9). End A.
+Section A. Global Notation "'Z'" := O (at level 9). End A.
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e7a66203cf..14bcb1ef78 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -337,3 +337,62 @@ type vernac_expr =
   | VernacExtend of string * raw_generic_argument list
 
 and located_vernac_expr = loc * vernac_expr
+
+(* Managing locality *)
+
+let locality_flag = ref None
+
+let local_of_bool = function true -> Local | false -> Global
+
+let check_locality () =
+  if !locality_flag = Some true then
+    error "This command does not support the \"Local\" prefix";
+  if !locality_flag = Some false then
+    error "This command does not support the \"Global\" prefix"
+
+let use_locality () =
+  let local = match !locality_flag with Some true -> true | _ -> false in
+  locality_flag := None;
+  local
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let use_section_locality () =
+  let local = 
+    match !locality_flag with Some b -> b | None -> Lib.sections_are_opened ()
+  in
+  locality_flag := None;
+  local
+
+let use_non_locality () =
+  let local = match !locality_flag with Some false -> false | _ -> true in
+  locality_flag := None;
+  local
+
+let enforce_locality () =
+  let local =
+    match !locality_flag with 
+    | Some false ->
+	error "Cannot be simultaneously Local and Global"
+    | _ -> 
+	Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix"; 
+	true in
+  locality_flag := None;
+  local
+
+let enforce_locality_exp () = local_of_bool (enforce_locality ())
+
+let enforce_locality_of local =
+  let local = 
+    match !locality_flag with 
+    | Some false when local ->
+	error "Cannot be simultaneously Local and Global"
+    | Some true when local ->
+	error "Use only prefix \"Local\""
+    | None ->
+	if local then
+	  Flags.if_verbose Pp.warning "Obsolete syntax: use \"Local\" prefix";
+	local
+    | Some b -> b in
+  locality_flag := None;
+  local