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/recordops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a8e934d3c6..c26da8ccc7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -185,7 +185,7 @@ let rec cs_pattern_of_constr env t =
   | Rel n -> Default_cs, Some n, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
   | Proj (p, c) ->
-    let { Environ.uj_type = ty } = Typeops.infer env c in
+    let ty = Retyping.get_type_of_constr env c in
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
-- 
cgit v1.2.3