diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 17:38:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 08:58:19 +0100 |
| commit | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (patch) | |
| tree | dd5e6675dcc46209f1ac33dad40292e85450ff1f /pretyping/inductiveops.mli | |
| parent | f4002e6c85f575fc8451adb80dba705795f0a0c9 (diff) | |
An example in centralizing similar functions to a common place so that
cleaning the interfaces is eventually easier. Here, adding
find_mrectype_vect to simplify vnorm.ml.
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 757599a3c..9036f521e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -159,6 +159,7 @@ val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : constr -> pinductive * constr list val find_mrectype : env -> evar_map -> types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array val find_rectype : env -> evar_map -> types -> inductive_type val find_inductive : env -> evar_map -> types -> pinductive * constr list val find_coinductive : env -> evar_map -> types -> pinductive * constr list |