diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 8631f5545..900a96829 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -34,5 +34,5 @@ val get_assumption_of : env -> evar_map -> constr -> types (* Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -val type_of_applied_inductive : env -> evar_map -> inductive -> +val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types |