From f8023074b3a82e8c8adb4ee380c07a68bdea5961 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Oct 2014 16:55:28 +0200
Subject: Make use of unfolded primitive projections when elaborating match on
 a primitive record.

---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 27340fe718..411f2c550f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1313,7 +1313,7 @@ let mk_case pb (ci,pred,c,brs) =
     match mib.mind_record with
     | Some (Some (_, cs, pbs)) ->
       Reduction.beta_appvect brs.(0) 
-	(Array.map (fun p -> mkProj (Projection.make p false, c)) cs)
+	(Array.map (fun p -> mkProj (Projection.make p true, c)) cs)
     | _ -> mkCase (ci,pred,c,brs)
 
 (**********************************************************************)
-- 
cgit v1.2.3