From e4aa8f13680a81ec7e2ebe1281b20d5791d13440 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 19:21:35 +0200
Subject: Fix universe instantiation with canonical structures.

Patch by Matthieu Sozeau.

Fixes #3819: "Error: Unsatisfied constraints" due to canonical
structure inference
---
 pretyping/recordops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6dc0d1f3c2..7fde7b7ac4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -190,7 +190,7 @@ let cs_pattern_of_constr t =
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
-  let ctx = Environ.constant_context env con in
+  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
-- 
cgit v1.2.3