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

4 files changed, 12 insertions, 6 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8415f0bcc9..54de06c9c8 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 e228b829ac..e2a3e33a2f 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 1b89eaa685..2e01aa3ea7 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 259329a104..7351249cdf 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