diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 21 |
1 files changed, 8 insertions, 13 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7587bd165f..3e1e9ceaf1 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Vernacexpr open Constrexpr @@ -42,22 +41,18 @@ val do_mutual_inductive val make_cases : Names.inductive -> string list list +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> DeclareInd.one_inductive_impls list + -> Names.MutInd.t + [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) -(** 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 -> - mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> - MutInd.t - val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the |