diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 900a96829..32b90cd86 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -36,3 +36,6 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types + +val type_of_constant_knowing_parameters : env -> evar_map -> constant -> + constr array -> types |