diff options
| author | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-29 10:20:32 +0200 |
| commit | 61aeca9ca2a7c46b143b90583dfb84b037eccc5b (patch) | |
| tree | 936cab27bacc3bb779aff810be7b79425544f10d /vernac/comInductive.mli | |
| parent | 6e5fee168d874b7b6fe7d5c8f4384661bf328d79 (diff) | |
| parent | c62aa0e9d0c33a70822e66a422d4c5926a8c8df7 (diff) | |
Merge PR #12372: [declare] Refactor constant information into a record.
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 984581152a..9c876787a3 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -41,14 +41,6 @@ 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"] - val interp_mutual_inductive_constr : sigma:Evd.evar_map -> template:bool option |