From fc7264feee8ee62aeda8af4d756deb009f29fc2b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 11:13:21 +0100
Subject: Try eta-expansion of records only on non-recursive ones

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 03a700e176..15e8022af0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -629,7 +629,7 @@ let is_eta_constructor_app env ts f l1 term =
   | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite &&
+      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite &&
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env ts term
-- 
cgit v1.2.3