From 8b257187f9b7ec95017a2df14b49c057d254ad15 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Oct 2014 15:17:58 +0200
Subject: Build unfolded versions of the primitive projection in let (a, p) :=
 ... to maintain compatibility (HoTT bug #557).

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

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6e32d70c09..d566dd9b23 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -104,8 +104,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	| None -> mkCase (ci, lift ndepar p,  mkRel 1,
 			  Termops.rel_vect ndepar k)
 	| Some ps -> 
-	  let term = mkApp (mkRel 2, 
-			    Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
+	  let term = 
+	    mkApp (mkRel 2, 
+		   Array.map 
+		   (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in
 	    if dep then
 	      let ty = mkApp (mkRel 3, [| mkRel 1 |]) in 
 		mkCast (term, DEFAULTcast, ty)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b20af031df..5383101b49 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -707,7 +707,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	let rec aux n k names l =
 	  match names, l with
 	  | na :: names, ((_, None, t) :: l) -> 
-	    let proj = Projection.make ps.(cs.cs_nargs - k) false in
+	    let proj = Projection.make ps.(cs.cs_nargs - k) true in
 	      (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t)
 	    :: aux (n+1) (k + 1) names l
 	  | na :: names, ((_, c, t) :: l) -> 
-- 
cgit v1.2.3