diff options
| author | Pierre-Marie Pédrot | 2019-07-29 13:13:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-29 13:13:58 +0200 |
| commit | e34fe0ab41143817f8dfd465ba18eaa6039b3c2f (patch) | |
| tree | 98d5fbbd8c65e77a43c5a4218e1b4b3e510a7d8f /vernac/comInductive.ml | |
| parent | bbec12e3bb2cd1062bd833bbb2c44adbeef33503 (diff) | |
| parent | e9a6a3115d801140663c15341662918d9645681c (diff) | |
Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 65db4401d9..664010c917 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -80,9 +80,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (Id.print x ++ str " is defined") @@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite - (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 |