diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 32b90cd86..6dbd426b2 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -34,8 +34,6 @@ 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_inductive_knowing_parameters : env -> evar_map -> inductive -> - constr array -> types - -val type_of_constant_knowing_parameters : env -> evar_map -> constant -> +val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types + |