Improved the treatment of Local/Global options (noneffective Local on

Implicit Arguments, Arguments Scope and Coercion fixed, noneffective
Global in sections for Hints and Notation detected).

Misc. improvements (comments + interpretation of Hint Constructors +
dev printer for hint_db).



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

16 files changed, 101 insertions, 29 deletions

diff --git a/dev/include b/dev/include
index 6ed62e1e9..6e25ef51e 100644
--- a/dev/include
+++ b/dev/include
@@ -23,6 +23,7 @@
 #install_printer  (* type_judgement *) pptype;;
 #install_printer  (* judgement *) ppj;;
 
+#install_printer  (* hint_db *)  print_hint_db;;
 #install_printer  (* goal *)  ppgoal;;
 #install_printer  (* sigma goal *)  ppsigmagoal;;
 #install_printer  (* proof *)  pproof;;
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 77eb29285..a5678eacf 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -747,13 +747,16 @@ to these arguments.
 
 This behaves like {\tt Arguments Scope} {\qualid} {\tt [
 \nelist{\optscope}{} ]} but survives when a section is closed instead
-of stopping working at section closing.
+of stopping working at section closing. Without the {\tt Global} modifier,
+the effect of the command stops when the section it belongs to ends.
 
 \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
-stops when the section it belongs to ends.
+This behaves like {\tt Arguments Scope} {\qualid} {\tt [
+    \nelist{\optscope}{} ]} but does not survive modules and files.
+Without the {\tt Local} modifier, the effect of the command is
+visible from within other modules or files.
+
 \end{Variants}
 
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 8f9f0959d..e3eb38af6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -475,6 +475,9 @@ let discharge_arguments_scope (_,(req,r,l)) =
   if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
   else Some (req,Lib.discharge_global r,l)
 
+let classify_arguments_scope (req,_,_ as obj) =
+  if req = ArgsScopeNoDischarge then Dispose else Substitute obj
+
 let rebuild_arguments_scope (req,r,l) =
   match req with
     | ArgsScopeNoDischarge -> assert false
@@ -492,7 +495,7 @@ let (inArgumentsScope,outArgumentsScope) =
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
-      classify_function = (fun o -> Substitute o);
+      classify_function = classify_arguments_scope;
       discharge_function = discharge_arguments_scope;
       rebuild_function = rebuild_arguments_scope }
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 1edac69aa..dec961793 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -521,6 +521,9 @@ let rebuild_implicits (req,l) =
 	  let l' = merge_impls auto m in [ref,l']
   in (req,l')
 
+let classify_implicits (req,_ as obj) =
+  if req = ImplLocal then None else Some obj
+
 let (inImplicits, _) =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f66b4ed1e..28a66182c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -812,7 +812,7 @@ GEXTEND Gram
 
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 opt_scope; "]" ->
-	 VernacArgumentsScope (use_non_locality (),qid,scl)
+	 VernacArgumentsScope (use_section_non_locality (),qid,scl)
 
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_string; ":="; p = constr;
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9406a57d7..7fa80b9a4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1286,7 +1286,7 @@ let matx_of_eqns env tomatchl eqns =
 
    We then look for a type U(..a1jk..b1 .. ..amjk..bm) so that
    T = U(..v1jk..t1 .. ..vmjk..tm). This a higher-order matching
-   problem with a priori different solution (one of them if T itself!).
+   problem with a priori different solutions (one of them if T itself!).
 
    We finally invert the uij and the ti and build the return clause
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7ec77f7dc..237963258 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -377,12 +377,15 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
 	  discharge_cl clt,
           n + ps)
 
+let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
+  if stre = Local then Dispose else Substitute obj
+
 let (inCoercion,_) =
   declare_object {(default_object "COERCION") with
     load_function = load_coercion;
     cache_function = cache_coercion;
     subst_function = subst_coercion;
-    classify_function = (fun x -> Substitute x);
+    classify_function = classify_coercion;
     discharge_function = discharge_coercion }
 
 let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index de1e3d2bd..287794bff 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -79,7 +79,7 @@ let disch_ref ref =
       EvalConstRef c ->
         let c' = Lib.discharge_con c in
         if c==c' then Some ref else Some (EvalConstRef c')
-    | _ -> Some ref
+    | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref
 
 let discharge_strategy (_,(local,obj)) =
   if local then None else
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fafc0b592..dd11e1ef0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -465,6 +465,16 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
 let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
+let discharge_autohint (_,(local,name,hintlist as obj)) =
+  if local then None else
+    match hintlist with
+    | CreateDB _ ->
+	(* We assume that the transparent state is either empty or full *)
+	Some obj
+    | AddTransparency _ | AddTactic _ ->
+	(* Needs the adequate code here to support Global Hints in sections *)
+	None
+
 let (inAutoHint,_) =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
@@ -560,7 +570,7 @@ let interp_hints h =
       HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
-        let ind = global_inductive qid in
+        let ind = global_inductive_with_alias qid in
         list_tabulate (fun i -> None, true, mkConstruct (ind,i+1))
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
diff --git a/test-suite/check b/test-suite/check
index a73654bcd..efac178c0 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -3,9 +3,9 @@
 # Automatic test of Coq
 
 if [ "$1" = -byte ]; then
-  coqtop="../bin/coqtop.byte -boot -q -batch"
+  coqtop="../bin/coqtop.byte -boot -q -batch -I prerequisite"
 else
-  coqtop="../bin/coqtop -boot -q -batch"
+  coqtop="../bin/coqtop -boot -q -batch -I prerequisite"
 fi
 
 command="$coqtop -top Top -load-vernac-source"
diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v
new file mode 100644
index 000000000..0a69b8517
--- /dev/null
+++ b/test-suite/failure/ImportedCoercion.v
@@ -0,0 +1,7 @@
+(* Test visibility of coercions *)
+
+Require Import make_local.
+
+(* Local coercion must not be used *)
+
+Check (0 = true).
diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v
new file mode 100644
index 000000000..cdb7a2691
--- /dev/null
+++ b/test-suite/prerequisite/make_local.v
@@ -0,0 +1,10 @@
+(* Used in Import.v to test the locality flag *)
+
+Definition f (A:Type) (a:A) := a.
+
+Local Arguments Scope f [type_scope type_scope].
+Local Implicit Arguments f [A].
+
+(* Used in Import.v to test the locality flag *)
+
+Local Coercion g (b:bool) := if b then 0 else 1.
diff --git a/test-suite/success/Import.v b/test-suite/success/Import.v
new file mode 100644
index 000000000..ff5c1ed75
--- /dev/null
+++ b/test-suite/success/Import.v
@@ -0,0 +1,11 @@
+(* Test visibility of imported objects *)
+
+Require Import make_local.
+
+(* Check local implicit arguments are not imported *)
+
+Check (f nat 0).
+
+(* Check local arguments scopes are not imported *)
+
+Check (f nat (0*0)).
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index b09c6c9a7..7d7bcc71e 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -30,7 +30,7 @@ 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. Global Notation "'Z'" := O (at level 9). End A.
+Section A. Require Import make_notation. End A.
 
 (* Check use of "$" (see bug #1961) *)
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 61fd743dc..b1cd5bfa5 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -64,8 +64,8 @@ Module KeyDecidableType(D:DecidableType).
   Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-  Global Hint Unfold eqk eqke.
-  Global Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold eqk eqke.
+  Hint Extern 2 (eqke ?a ?b) => split.
 
    (* eqke is stricter than eqk *)
 
@@ -88,19 +88,19 @@ Module KeyDecidableType(D:DecidableType).
    red; unfold eqke; intuition; [ eauto | congruence ].
   Qed.
 
-  Global Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
-  Global Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
-  Global Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
-  Global Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
-  Global Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
-  Global Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
+  Hint Resolve (@Equivalence_Reflexive _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqk_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqk_equiv).
+  Hint Resolve (@Equivalence_Reflexive _ _ eqke_equiv).
+  Hint Resolve (@Equivalence_Transitive _ _ eqke_equiv).
+  Hint Immediate (@Equivalence_Symmetric _ _ eqke_equiv).
 
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
     unfold eqke; induction 1; intuition.
   Qed.
-  Global Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
@@ -110,7 +110,7 @@ Module KeyDecidableType(D:DecidableType).
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
 
-  Global Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6a64fb1d5..96960540b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -132,6 +132,7 @@ type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
+type full_locality_flag = bool option (* true = Local; false = Global      *)
 
 type option_value =
   | StringValue of string
@@ -302,8 +303,8 @@ type vernac_expr =
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of
       locality_flag * (Conv_oracle.level * reference or_by_notation list) list
-  | VernacUnsetOption of bool option * Goptions.option_name
-  | VernacSetOption of bool option * Goptions.option_name * option_value
+  | VernacUnsetOption of full_locality_flag * Goptions.option_name
+  | VernacSetOption of full_locality_flag * 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
@@ -376,6 +377,9 @@ let use_section_locality () =
 let use_non_locality () =
   match use_locality_full () with Some false -> false | _ -> true
 
+let use_section_non_locality () =
+  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
+
 let enforce_locality () =
   let local =
     match !locality_flag with
@@ -388,9 +392,12 @@ let enforce_locality () =
   locality_flag := None;
   local
 
+(* [enforce_locality_exp] supports Local (with effect in section) but not
+   Global in section *)
+
 let enforce_locality_exp () = local_of_bool (enforce_locality ())
 
-let enforce_locality_of local =
+let enforce_full_locality_of local =
   let local =
     match !locality_flag with
     | Some false when local ->
@@ -398,10 +405,24 @@ let enforce_locality_of local =
     | Some true when local ->
 	error "Use only prefix \"Local\"."
     | None ->
-	if local then
+	if local then begin
 	  Flags.if_verbose
 	    Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
-	local
-    | Some b -> b in
+	  Some true
+	end else
+	None
+    | Some _ as b -> b in
   locality_flag := None;
   local
+
+(* [enforce_locality_of] supports Local (with effect if not in
+   section) but not Global in section *)
+
+let enforce_locality_of local =
+  match enforce_full_locality_of local with
+    | Some false ->
+	if Lib.sections_are_opened () then
+	  error "This command does not support the Global option in sections.";
+	false
+    | Some true -> true 
+    | None -> false