From 313e6bed17b400d638401a5c6e5d442eadb73d3a Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 4 Jun 2018 15:47:28 -0700 Subject: Implement uniform parameters in ComInductive Don't allow notations attached to uniform inductives --- vernac/comInductive.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'vernac/comInductive.mli') diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7ae8e8f71..4e30ed7de 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -19,9 +19,14 @@ open Decl_kinds (** Entry points for the vernacular commands Inductive and CoInductive *) +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + Declarations.recursivity_kind -> unit (************************************************************************) (** Internal API *) -- cgit v1.2.3