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.

---
 pretyping/detyping.ml  | 3 ++-
 pretyping/detyping.mli | 8 ++++----
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a91c4f5ac1..2df1975461 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -487,8 +487,9 @@ let rec detype flags avoid env sigma t =
 	      let pb = Environ.lookup_projection p (snd env) in
 	      let body = pb.Declarations.proj_body in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
-	      let (ind, args) = Inductiveops.find_mrectype (snd env) sigma ty in
+	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
+	      let body' = subst_instance_constr u body' in
 		substl (c :: List.rev args) body'
 	    with Retyping.RetypeError _ | Not_found -> 
 	      anomaly (str"Cannot detype an unfolded primitive projection.")
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index b9fdb5cbe4..725fff5b2c 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -36,12 +36,12 @@ val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> cons
 val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr
 
 val detype_case :
-  bool -> ('a -> glob_constr) ->
-  (constructor array -> bool list array -> 'a array ->
+  bool -> (constr -> glob_constr) ->
+  (constructor array -> bool list array -> constr array ->
     (Loc.t * Id.t list * cases_pattern list * glob_constr) list) ->
-  ('a -> bool list -> bool) ->
+  (constr -> bool list -> bool) ->
   Id.t list -> inductive * case_style * bool list array * bool list ->
-    'a option -> 'a -> 'a array -> glob_constr
+    constr option -> constr -> constr array -> glob_constr
 
 val detype_sort : sorts -> glob_sort
 
-- 
cgit v1.2.3