diff options
| author | Gaëtan Gilbert | 2020-07-02 15:30:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-05 21:03:17 +0200 |
| commit | 1e92ed4d129aea5ea4e9300a24e1135cc186c341 (patch) | |
| tree | c78ff50d0d156a54b950aaf7b1a80b36b2e23b14 /pretyping/retyping.mli | |
| parent | cea10e4e16c05b06693184425dd70ce6e5eba8a8 (diff) | |
Fix Canonical with universe polymorphism and primitive projection
Perhaps we should thread an evar map with the Var universes added
through to cs_pattern_of_constr but that would be significantly more invasive.
Fix #12528
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 |