diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 83393572..4e30ed7d 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 *) @@ -37,7 +42,7 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val declare_mutual_inductive_with_eliminations : - mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> + mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> MutInd.t (** Exported for Funind *) @@ -64,4 +69,4 @@ val extract_mutual_inductive_declaration_components : val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> polymorphic -> private_flag -> Declarations.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list + mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list |