diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-08 09:16:42 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-08 09:16:42 +0000 |
| commit | a26efb5269114b8c23f823b9eabcccbdc71a6e92 (patch) | |
| tree | fc83958cf7c76678e18b80f9a6a47ba0d2c172f2 /kernel/vconv.ml | |
| parent | 8e4b7319caa0754401c8b868e9ce9490a867d7f1 (diff) | |
adding eta in the vm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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), _ -> |