diff options
Diffstat (limited to 'vernac/declareInd.mli')
| -rw-r--r-- | vernac/declareInd.mli | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index 6db09ad2bd..df8895a999 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -8,7 +8,16 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : Entries.mutual_inductive_entry -> Libobject.object_name * bool +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> one_inductive_impls list + -> Names.MutInd.t |