diff options
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), _ -> |