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 c7901e949..52e5d7049 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -26,7 +26,7 @@ val get_sort_of : env -> evar_map -> types -> sorts val get_sort_family_of : env -> evar_map -> types -> sorts_family val get_type_of_with_meta : - env -> evar_map -> Termops.metamap -> constr -> types + env -> evar_map -> Termops.meta_type_map -> constr -> types (* Makes an assumption from a constr *) val get_assumption_of : env -> evar_map -> constr -> types |