diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 9d67089f78..2bc8136787 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -14,6 +14,17 @@ open Declarations open Environ open Evd +(* The following three functions are similar to the ones defined in + Inductive, but they expect an env *) + +val type_of_inductive : env -> inductive -> types + +(* Return type as quoted by the user *) +val type_of_constructor : env -> constructor -> types + +(* Return constructor types in normal form *) +val arities_of_constructors : env -> inductive -> types array + (* An inductive type with its parameters *) type inductive_family val make_ind_family : inductive * constr list -> inductive_family |