From 37a58edffeff7b6a7f03ec781e1e2ca73de4b3af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 14 Aug 2014 13:01:30 +0200
Subject: Restrict eta-conversion to inductive records, fixing bug #3310.

---
 kernel/closure.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 62ee5db5d5..6dacb7818c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -866,7 +866,8 @@ let rec get_parameters depth n argstk =
 let eta_expand_ind_stacks env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (exp,projs) when Array.length projs > 0 -> 
+    | Some (exp,projs) when Array.length projs > 0 
+      && mib.Declarations.mind_finite -> 
       let primitive = Environ.is_projection projs.(0) env in
 	if primitive then
 	  (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-- 
cgit v1.2.3