Granting bug #3098: adding priority to Existing Instances.

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

6 files changed, 22 insertions, 14 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index a780ac0f1..bbb68689c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -297,7 +297,8 @@ type vernac_expr =
 
   | VernacContext of local_binder list
 
-  | VernacDeclareInstances of reference list (* instance names *)
+  | VernacDeclareInstances of
+    reference list * int option (* instance names, priority *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 450414625..aac47126f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -560,10 +560,12 @@ GEXTEND Gram
 	     ":="; c = lconstr -> Some c | -> None ] ->
 	   VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri)
 
-      | IDENT "Existing"; IDENT "Instance"; id = global ->
-	  VernacDeclareInstances [id]
-      | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global ->
-	  VernacDeclareInstances ids
+      | IDENT "Existing"; IDENT "Instance"; id = global;
+          pri = OPT [ "|"; i = natural -> i ] ->
+	  VernacDeclareInstances ([id], pri)
+      | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
+          pri = OPT [ "|"; i = natural -> i ] ->
+	  VernacDeclareInstances (ids, pri)
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3c4f25880..3e6fa4861 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -381,6 +381,10 @@ let pr_statement head (id,(bl,c,guard)) =
     pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
     str":" ++ pr_spc_lconstr c)
 
+let pr_priority = function
+| None -> mt ()
+| Some i -> spc () ++ str "|" ++ spc () ++ int i
+
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
@@ -714,7 +718,7 @@ let rec pr_vernac = function
 	Anonymous -> mt ()) ++
        pr_and_type_binders_arg sup ++
        str":" ++ spc () ++
-       pr_constr cl ++ spc () ++
+       pr_constr cl ++ pr_priority pri ++
 	 (match props with
 	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr p
 	  | None -> mt()))
@@ -724,10 +728,10 @@ let rec pr_vernac = function
        str"Context" ++ spc () ++ pr_and_type_binders_arg l)
 
 
- | VernacDeclareInstances ids ->
+ | VernacDeclareInstances (ids, pri) ->
      hov 1 ( str"Existing" ++ spc () ++ 
              str(String.plural (List.length ids) "Instance") ++
-             spc () ++ prlist_with_sep spc pr_reference ids)
+             spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
 
  | VernacDeclareClass id ->
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3f56f80dc..e4064049e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -53,12 +53,12 @@ let declare_class g =
 		      Pp.str"Unsupported class type, only constants and inductives are allowed")
     
 (** TODO: add subinstances *)
-let existing_instance glob g =
+let existing_instance glob g pri =
   let c = global g in
   let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some (_, (tc, _)) -> add_instance (new_instance tc None glob c)
+      | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob c)
       | None -> user_err_loc (loc_of_reference g, "declare_instance",
 			     Pp.str "Constant does not build instances of a declared type class.")
 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 0a71921b0..1d9ae6ec4 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -32,7 +32,8 @@ val declare_class : reference -> unit
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> unit
+val existing_instance : bool -> reference -> int option -> unit
+(** globality, reference, priority *)
 
 val declare_instance_constant :
   typeclass ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ffc53f55b..103253c52 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -807,9 +807,9 @@ let vernac_instance abst locality sup inst props pri =
 let vernac_context l =
   if not (Classes.context l) then Pp.feedback Interface.AddedAxiom
 
-let vernac_declare_instances locality ids =
+let vernac_declare_instances locality ids pri =
   let glob = not (make_section_locality locality) in
-  List.iter (fun (id) -> Classes.existing_instance glob id) ids
+  List.iter (fun id -> Classes.existing_instance glob id pri) ids
 
 let vernac_declare_class id =
   Classes.declare_class id
@@ -1787,7 +1787,7 @@ let interp locality c = match c with
   | VernacInstance (abst, sup, inst, props, pri) ->
       vernac_instance abst locality sup inst props pri
   | VernacContext sup -> vernac_context sup
-  | VernacDeclareInstances ids -> vernac_declare_instances locality ids
+  | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)