From 32c83676c96ae4a218de0bec75d2f3353381dfb3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 28 Aug 2014 19:49:16 +0200
Subject: Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 498b33b632..d2e95a74b6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -215,7 +215,7 @@ let oib_equal o1 o2 =
     Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let eq_record x y =
-  Option.equal (fun (x, y) (x', y') -> eq_constr x x') x y
+  Option.equal (fun (x, y) (x', y') -> Array.for_all2 eq_constant x x') x y
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
-- 
cgit v1.2.3