From 3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 6 Sep 2014 12:13:03 +0200
Subject: Fix bug #3584, elaborating pattern-matching on primitive records to
 the use of projections.

---
 pretyping/cases.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 560289d1ee..f9bd2d4058 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1277,6 +1277,13 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
 
 *)
 
+let mk_case pb (ci,pred,c,brs) =
+  let mib = lookup_mind (fst ci.ci_ind) pb.env in
+    match mib.mind_record with
+    | Some (cs, pbs) when Array.length pbs > 0 -> 
+      Reduction.beta_appvect brs.(0) (Array.map (fun p -> mkProj (p, c)) cs)
+    | _ -> mkCase (ci,pred,c,brs)
+
 (**********************************************************************)
 (* Main compiling descent *)
 let rec compile pb =
@@ -1323,7 +1330,7 @@ and match_current pb (initial,tomatch) =
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
 	  let pred = nf_betaiota !(pb.evdref) pred in
-	  let case = mkCase (ci,pred,current,brvals) in
+	  let case = mk_case pb (ci,pred,current,brvals) in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
-- 
cgit v1.2.3