Add 'Existing Instances' declaration to declare multiple instances at once.

This is useful, for example, in declaring the projection of the dependent
record bundled form of an unbundled typeclass.

Patch submitted by Tom Prince

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

7 files changed, 20 insertions, 11 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7bd4f3522d..20ff649aac 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -367,6 +367,12 @@ instances at the end of sections, or declaring structure projections as
 instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
   typeclass\_instances}.
 
+\begin{Variants}
+\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$}
+  \comindex{Existing Instances}
+  With this command, several existing instances can be declared at once.
+\end{Variants}
+
 \subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}}
 \comindex{Context}
 \label{Context}
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 406d152cd6..7f91ceee68 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -86,7 +86,7 @@ let sentence_sep = '.' [ ' ' '\r' '\n' '\t' ]
 let multiword_declaration =
   "Module" (space+ "Type")?
 | "Program" space+ ident
-| "Existing" space+ "Instance"
+| "Existing" space+ "Instance" "s"?
 | "Canonical" space+ "Structure"
 
 let locality = ("Local" space+)?
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f405600064..160d94130f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -560,8 +560,10 @@ GEXTEND Gram
 	   VernacInstance (false, not (use_section_locality ()),
 			   snd namesup, (fst namesup, expl, t), props, pri)
 
-      | IDENT "Existing"; IDENT "Instance"; is = global -> 
-	  VernacDeclareInstance (not (use_section_locality ()), is)
+      | IDENT "Existing"; IDENT "Instance"; id = global ->
+	  VernacDeclareInstances (not (use_section_locality ()), [id])
+      | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global ->
+	  VernacDeclareInstances (not (use_section_locality ()), ids)
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9578dc7cec..4bf6e59f13 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -709,9 +709,10 @@ let rec pr_vernac = function
 	 pr_and_type_binders_arg l ++ spc () ++ str "]")
 
 
- | VernacDeclareInstance (glob, id) ->
+ | VernacDeclareInstances (glob, ids) ->
      hov 1 (pr_non_locality (not glob) ++
-	       str"Existing" ++ spc () ++ str"Instance" ++ spc () ++ pr_reference id)
+               str"Existing" ++ spc () ++ str(plural (List.length ids) "Instance") ++
+               spc () ++ prlist_with_sep spc pr_reference ids)
 
  | VernacDeclareClass id ->
      hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_reference id)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4d7b8f5291..e2d22472a0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -90,7 +90,7 @@ let rec attribute_of_vernac_command = function
   (* Type classes *)
   | VernacInstance _ -> []
   | VernacContext _ -> []
-  | VernacDeclareInstance _ -> []
+  | VernacDeclareInstances _ -> []
   | VernacDeclareClass _ -> []
 
   (* Solving *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index faa21850d7..938b59a9b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -635,8 +635,8 @@ let vernac_instance abst glob sup inst props pri =
 let vernac_context l =
   Classes.context l
 
-let vernac_declare_instance glob id =
-  Classes.declare_instance glob id
+let vernac_declare_instances glob ids =
+  List.iter (fun (id) -> Classes.declare_instance glob id) ids
 
 let vernac_declare_class id =
   Classes.declare_class id
@@ -1368,7 +1368,7 @@ let interp c = match c with
   | VernacInstance (abst, glob, sup, inst, props, pri) ->
       vernac_instance abst glob sup inst props pri
   | VernacContext sup -> vernac_context sup
-  | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id
+  | VernacDeclareInstances (glob, ids) -> vernac_declare_instances glob ids
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6858de706f..216306f5e7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -260,8 +260,8 @@ type vernac_expr =
 
   | VernacContext of local_binder list
 
-  | VernacDeclareInstance of
-      bool (* global *) * reference (* instance name *)
+  | VernacDeclareInstances of
+      bool (* global *) * reference list (* instance names *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)