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 be42fd858..9b65494c1 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -21,7 +21,7 @@ open Environ either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) -val get_type_of : env -> evar_map -> constr -> types +val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types val get_sort_of : env -> evar_map -> types -> sorts val get_sort_family_of : env -> evar_map -> types -> sorts_family |