From 1e92ed4d129aea5ea4e9300a24e1135cc186c341 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:30:07 +0200
Subject: 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
---
 pretyping/retyping.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'pretyping/retyping.mli')

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
 
-- 
cgit v1.2.3