diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 18 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 11 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/typing.ml | 1 |
4 files changed, 31 insertions, 0 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cda1169dd7..74795f572c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -18,6 +18,24 @@ open Declarations open Environ open Reductionops +(* The following three functions are similar to the ones defined in + Inductive, but they expect an env *) + +let type_of_inductive env ind = + let specif = Inductive.lookup_mind_specif env ind in + Inductive.type_of_inductive specif + +(* Return type as quoted by the user *) +let type_of_constructor env cstr = + let specif = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Inductive.type_of_constructor cstr specif + +(* Return constructor types in normal form *) +let arities_of_constructors env ind = + let specif = Inductive.lookup_mind_specif env ind in + Inductive.arities_of_constructors ind specif + (* [inductive_family] = [inductive_instance] applied to global parameters *) type inductive_family = inductive * constr list 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 diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5a71b28d8d..a75e48a8e9 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -11,6 +11,7 @@ open Util open Term open Inductive +open Inductiveops open Names open Reductionops open Environ diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 759a0c1a15..2f34957022 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -16,6 +16,7 @@ open Reductionops open Type_errors open Pretype_errors open Inductive +open Inductiveops open Typeops let meta_type env mv = |