diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index c2a08f4b9..fc1dd3564 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -26,8 +26,7 @@ type retype_error exception RetypeError of retype_error val get_type_of : - ?polyprop:bool -> ?refresh:bool -> ?lax:bool -> - env -> evar_map -> constr -> types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> sorts |