From c60f40ccecf526b5c7ce5adfe5908fdac3f66771 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 13 Jan 2015 00:25:21 +0530
Subject: Fix issue in printing due to de Bruijn bug when constructing
 compatibility constr for primitive records (not used anywhere else than
 printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add
 some minor fixes in detyping and pretty printing related to universes.

---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 635c5c4bf6..99d9f52c96 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -683,7 +683,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
     let ccl' = liftn 1 2 ccl in
     let p = mkLambda (x, lift 1 rp, ccl') in
     let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
-    let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
       it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
   in
   let projections (na, b, t) (i, j, kns, pbs, subst) =
-- 
cgit v1.2.3