diff options
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 16bc251c2a..2e19ffdfcd 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -30,6 +30,10 @@ exception RetypeError of retype_error val get_type_of : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types +(** No-evar version of [get_type_of] *) +val get_type_of_constr : ?polyprop:bool -> ?lax:bool + -> env -> ?uctx:UState.t -> Constr.t -> Constr.types + val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t |