From e7ba2a9be24823503495e959f0dffc131e99801b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Jul 2014 18:51:13 +0200
Subject: Fix eta expansion of primitive records (HoTT bug #78), which now
 fails cleanly when called on partially applied constructors. Also protect
 evar_conv from that case.

---
 pretyping/evarconv.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e9d152de2d..cef8215866 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -708,7 +708,9 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
 		 exact_ise_stack2 env evd (evar_conv_x ts) l1' 
 		   (Stack.append_app_list l2' Stack.empty)
 	     else raise (Failure "")
-	 with Failure _ -> UnifFailure(evd,NotSameHead))
+	 with 
+	 | Invalid_argument _ (* Stack.tail: partially applied constructor *)
+	 | Failure _ -> UnifFailure(evd,NotSameHead))
     | _ -> UnifFailure (evd,NotSameHead)
 
 (* Profiling *)
-- 
cgit v1.2.3