diff options
author | 2013-05-08 18:01:07 +0200 | |
---|---|---|
committer | 2013-05-08 18:01:07 +0200 | |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /kernel/vconv.ml | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r-- | kernel/vconv.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index a35d1d88..4d0edc68 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), _ -> @@ -98,7 +100,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu = conv_stack k stk1 stk2 cu else raise NotConvertible with NotConvertible -> - if oracle_order ik1 ik2 then + if oracle_order false ik1 ik2 then conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu end @@ -219,12 +221,12 @@ and conv_eq_vect vt1 vt2 cu = let vconv pb env t1 t2 = let cu = - try conv_eq pb t1 t2 Constraint.empty + try conv_eq pb t1 t2 empty_constraint with NotConvertible -> infos := create_clos_infos betaiotazeta env; let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in - let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in + let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in cu in cu @@ -234,8 +236,8 @@ let use_vm = ref false let set_use_vm b = use_vm := b; - if b then Reduction.set_default_conv vconv - else Reduction.set_default_conv Reduction.conv_cmp + if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb) + else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb) let use_vm _ = !use_vm |