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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/retyping.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb518bc2f9..7a1af7f41a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -257,6 +257,9 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = (* Makes an unsafe judgment from a constr *) let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c } +let get_type_of_constr ?polyprop ?lax env ?(uctx=UState.from_env env) c = + EConstr.Unsafe.to_constr (get_type_of ?polyprop ?lax env (Evd.from_ctx uctx) (EConstr.of_constr c)) + (* Returns sorts of a context *) let sorts_of_context env evc ctxt = let rec aux = function |