Slight change in the semantics of arguments scopes: scopes can no

longer be bound to Funclass or Sortclass (this does not seem to be
useful). [An exception is when using modules, if a constant foo is
expanded into a type, a "Bind Scope sc with foo" starts binding
Sortclass].

Also reworked reference manual for Arguments Scopes and Bind Scopes.

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

10 files changed, 92 insertions, 49 deletions

diff --git a/CHANGES b/CHANGES
index cdcda4ed1..1fcca5888 100644
--- a/CHANGES
+++ b/CHANGES
@@ -30,6 +30,9 @@ CoqIDE
 - Coqide now supports the Restart command, and Undo (with a warning).
   Better support for Abort.
 
+Notations
+
+- "Bind Scope" can no longer bind "Funclass" and "Sortclass".
 
 Changes from V8.4beta to V8.4
 =============================
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ea3d55f2d..a3713eb36 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -802,10 +802,13 @@ put into the {\tt type\_scope} scope.
 Arguments respectful {A B}%type (R R')%signature _ _.
 \end{coq_example*}
 
-When interpreting a term, if some of the
-arguments of {\qualid} are built from a notation, then this notation
-is interpreted in the scope stack extended by the scopes bound (if any)
-to these arguments.
+When interpreting a term, if some of the arguments of {\qualid} are
+built from a notation, then this notation is interpreted in the scope
+stack extended by the scope bound (if any) to this argument. The
+effect of the scope is limited to the argument itself. It does not propagate 
+to subterms but the subterms that, after interpretation of the
+notation, turn to be themselves arguments of a reference are
+interpreted accordingly to the arguments scopes bound to this reference.
 
 Arguments scopes can be cleared with the following command:
 
@@ -830,7 +833,6 @@ visible from within other modules or files.
 
 \end{Variants}
 
-
 \SeeAlso The command to show the scopes bound to the arguments of a
 function is described in Section~\ref{About}.
 
@@ -838,20 +840,23 @@ function is described in Section~\ref{About}.
 
 When an interpretation scope is naturally associated to a type
 (e.g. the scope of operations on the natural numbers), it may be
-convenient to bind it to this type. The effect of this is that any
-argument of a function that syntactically expects a parameter of this
-type is interpreted using scope. More precisely, it applies only if
-this argument is built from a notation, and if so, this notation is
-interpreted in the scope stack extended by this particular scope.  It
-does not apply to the subterms of this notation (unless the
-interpretation of the notation itself expects arguments of the same
-type that would trigger the same scope).
-
-\comindex{Bind Scope}
-More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
-bound to an interpretation scope. The command to do it is
+convenient to bind it to this type. When a scope {\scope} is bound to
+a type {\type}, any new function defined later on gets its arguments
+of type {\type} interpreted by default in scope {\scope} (this default
+behavior can however be overwritten by explicitly using the command
+{\tt Arguments}).
+
+Whether the argument of a function has some type {\type} is determined
+statically. For instance, if {\tt f} is a polymorphic function of type
+{\tt forall X:Type, X -> X} and type {\tt t} is bound to a scope
+{\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
+recognized as an argument to be interpreted in scope {\scope}.
+
+\comindex{Bind Scope} 
+Any global reference can be bound by default to an
+interpretation scope. The command to do it is
 \begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\class}
+{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
 \end{quote}
 
 \Example
diff --git a/interp/notation.ml b/interp/notation.ml
index 397f46fc4..102d42c21 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -434,24 +434,31 @@ let isAVar_or_AHole = function AVar _ | AHole _ -> true | _ -> false
 (**********************************************************************)
 (* Mapping classes to scopes *)
 
-open Classops
+type scope_class = ScopeRef of global_reference | ScopeSort
 
-let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
+let scope_class_of_reference x = ScopeRef x
+
+let compute_scope_class t =
+  let t', _ = Reductionops.whd_betaiotazeta_stack Evd.empty t in
+  match kind_of_term t' with
+  | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
+  | Sort _ -> ScopeSort
+  |  _ -> raise Not_found
+
+let scope_class_map = ref (Gmap.empty : (scope_class,scope_name) Gmap.t)
 
 let _ =
-  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+  scope_class_map := Gmap.add ScopeSort "type_scope" Gmap.empty
 
-let declare_class_scope sc cl =
-  class_scope_map := Gmap.add cl sc !class_scope_map
+let declare_scope_class sc cl =
+  scope_class_map := Gmap.add cl sc !scope_class_map
 
-let find_class_scope cl =
-  Gmap.find cl !class_scope_map
+let find_scope_class cl =
+  Gmap.find cl !scope_class_map
 
-let find_class_scope_opt = function
+let find_scope_class_opt = function
   | None -> None
-  | Some cl -> try Some (find_class_scope cl) with Not_found -> None
-
-let find_class t = fst (find_class_type Evd.empty t)
+  | Some cl -> try Some (find_scope_class cl) with Not_found -> None
 
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
@@ -459,13 +466,13 @@ let find_class t = fst (find_class_type Evd.empty t)
 let rec compute_arguments_classes t =
   match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
     | Prod (_,t,u) ->
-	let cl = try Some (find_class t) with Not_found -> None in
+	let cl = try Some (compute_scope_class t) with Not_found -> None in
 	cl :: compute_arguments_classes u
     | _ -> []
 
 let compute_arguments_scope_full t =
   let cls = compute_arguments_classes t in
-  let scs = List.map find_class_scope_opt cls in
+  let scs = List.map find_scope_class_opt cls in
   scs, cls
 
 let compute_arguments_scope t = fst (compute_arguments_scope_full t)
@@ -494,12 +501,23 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) =
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
+let subst_scope_class subst cs = match cs with
+  | ScopeSort -> Some cs
+  | ScopeRef t ->
+      let (t',c) = subst_global subst t in
+      if t == t' then Some cs
+      else try Some (compute_scope_class c) with Not_found -> None
+
 let subst_arguments_scope (subst,(req,r,scl,cls)) =
   let r' = fst (subst_global subst r) in
-  let subst_cl cl =
-    try Option.smartmap (subst_cl_typ subst) cl with Not_found -> None in
+  let subst_cl ocl = match ocl with
+    | None -> ocl
+    | Some cl ->
+        match subst_scope_class subst cl with
+        | Some cl'  as ocl' when cl' != cl -> ocl'
+        | _ -> ocl in
   let cls' = list_smartmap subst_cl cls in
-  let scl' = merge_scope (List.map find_class_scope_opt cls') scl in
+  let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
   let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
   (ArgsScopeNoDischarge,r',scl'',cls')
 
@@ -525,7 +543,7 @@ let rebuild_arguments_scope (req,r,l,_) =
 
 type arguments_scope_obj =
     arguments_scope_discharge_request * global_reference *
-      scope_name option list * Classops.cl_typ option list
+      scope_name option list * scope_class option list
 
 let inArgumentsScope : arguments_scope_obj -> obj =
   declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -600,14 +618,18 @@ let pr_delimiters_info = function
   | Some key -> str "Delimiting key is " ++ str key
 
 let classes_of_scope sc =
-  Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !class_scope_map []
+  Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !scope_class_map []
+
+let pr_scope_class = function
+  | ScopeSort -> str "Sort"
+  | ScopeRef t -> pr_global_env Idset.empty t
 
 let pr_scope_classes sc =
   let l = classes_of_scope sc in
   if l = [] then mt()
   else
     hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
-      spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
+      spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
 
 let pr_notation_info prglob ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++
@@ -789,7 +811,7 @@ let find_notation_printing_rule ntn =
 let freeze () =
  (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
   !delimiters_map, !notations_key_table, !printing_rules,
-  !class_scope_map)
+  !scope_class_map)
 
 let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
   scope_map := scm;
@@ -799,7 +821,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
   arguments_scope := asc;
   notations_key_table := fkm;
   printing_rules := pprules;
-  class_scope_map := clsc
+  scope_class_map := clsc
 
 let init () =
   init_scope_map ();
@@ -811,7 +833,7 @@ let init () =
   delimiters_map := Gmap.empty;
   notations_key_table := Gmapl.empty;
   printing_rules := Gmap.empty;
-  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
+  scope_class_map := Gmap.add ScopeSort "type_scope" Gmap.empty
 
 let _ =
   declare_summary "symbols"
diff --git a/interp/notation.mli b/interp/notation.mli
index de14c9515..1a02bc8a2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -146,7 +146,13 @@ val declare_arguments_scope :
 
 val find_arguments_scope : global_reference -> scope_name option list
 
-val declare_class_scope : scope_name -> Classops.cl_typ -> unit
+type scope_class
+
+val scope_class_of_reference : global_reference -> scope_class
+val subst_scope_class :
+  Mod_subst.substitution -> scope_class -> scope_class option
+
+val declare_scope_class : scope_name -> scope_class -> unit
 val declare_ref_arguments_scope : global_reference -> unit
 
 val compute_arguments_scope : Term.types -> scope_name option list
@@ -163,6 +169,7 @@ val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
 (** Prints scopes (expects a pure aconstr printer) *)
+val pr_scope_class : scope_class -> std_ppcmds
 val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds
 val locate_notation : (glob_constr -> std_ppcmds) -> notation ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 38e4e8eec..336d1e178 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -971,7 +971,7 @@ GEXTEND Gram
 	 VernacDelimiters (sc,key)
 
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
-       refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
+       refl = LIST1 smart_global -> VernacBindScope (sc,refl)
 
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_lstring; ":="; p = constr;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 49c76c96c..f9f565dce 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -502,7 +502,7 @@ let rec pr_vernac = function
       spc() ++ str "with " ++ str key
   | VernacBindScope (sc,cll) ->
       str"Bind Scope" ++ spc () ++ str sc ++
-      spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll
+      spc() ++ str "with " ++ prlist_with_sep spc pr_smart_global cll
   | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function
       |	None -> str"_"
       |	Some sc -> str sc in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8415f0bcc..54de06c9c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1145,7 +1145,7 @@ let add_infix local ((loc,inf),modifiers) pr sc =
 (**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
 
-type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
+type scope_command = ScopeDelim of string | ScopeClasses of scope_class list
 
 let load_scope_command _ (_,(scope,dlm)) =
   Notation.declare_scope scope
@@ -1154,7 +1154,7 @@ let open_scope_command i (_,(scope,o)) =
   if i=1 then
     match o with
     | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
-    | ScopeClasses cl -> Notation.declare_class_scope scope cl
+    | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
 
 let cache_scope_command o =
   load_scope_command 1 o;
@@ -1162,7 +1162,10 @@ let cache_scope_command o =
 
 let subst_scope_command (subst,(scope,o as x)) = match o with
   | ScopeClasses cl ->
-      let cl' = Classops.subst_cl_typ subst cl in if cl'==cl then x else
+      let cl' = list_map_filter (subst_scope_class subst) cl in
+      let cl' =
+        if List.length cl = List.length cl' && List.for_all2 (==) cl cl' then cl
+        else cl' in
       scope, ScopeClasses cl'
   | _ -> x
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index e228b829a..e2a3e33a2 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -35,7 +35,7 @@ val add_notation : locality_flag -> constr_expr ->
 (** Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
-val add_class_scope : scope_name -> Classops.cl_typ -> unit
+val add_class_scope : scope_name -> scope_class list -> unit
 
 (** Add only the interpretation of a notation that already has pa/pp rules *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1b89eaa68..2e01aa3ea 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -59,6 +59,9 @@ let cl_of_qualid = function
   | SortClass -> Classops.CL_SORT
   | RefClass r -> Class.class_of_global (Smartlocate.smart_global r)
 
+let scope_class_of_qualid qid =
+  Notation.scope_class_of_reference (Smartlocate.smart_global qid)
+
 (*******************)
 (* "Show" commands *)
 
@@ -320,7 +323,7 @@ let vernac_syntax_extension = Metasyntax.add_syntax_extension
 let vernac_delimiters = Metasyntax.add_delimiters
 
 let vernac_bind_scope sc cll =
-  List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll
+  Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
 
 let vernac_open_close_scope = Notation.open_close_scope
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 259329a10..7351249cd 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -225,7 +225,7 @@ type vernac_expr =
   | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * string
-  | VernacBindScope of scope_name * class_rawexpr list
+  | VernacBindScope of scope_name * reference or_by_notation list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of