From a26efb5269114b8c23f823b9eabcccbdc71a6e92 Mon Sep 17 00:00:00 2001
From: bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 8 Mar 2011 09:16:42 +0000
Subject: adding eta in the vm

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/vconv.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 96445f696..bf3640e35 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -74,6 +74,8 @@ and conv_whd pb k whd1 whd2 cu =
       else raise NotConvertible
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom pb k a1 stk1 a2 stk2 cu
+  | Vfun _, _ | _, Vfun _ ->
+      conv_val CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
   | _, Vatom_stk(Aiddef(_,v),stk) ->
       conv_whd pb k whd1 (force_whd v stk) cu
   | Vatom_stk(Aiddef(_,v),stk), _ ->
-- 
cgit v1.2.3