diff options
| -rw-r--r-- | doc/refman/Classes.tex | 6 | ||||
| -rw-r--r-- | ide/coq_lex.mll | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 5 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
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 *) |