diff options
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 4610dbcb..74d956be 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -1,13 +1,9 @@ open Util open Names -open Term open Environ -open Conv_oracle open Reduction -open Closure open Vm open Csymtable -open Univ let val_of_constr env c = val_of_constr (pre_env env) c @@ -81,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu = | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> + (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ @@ -120,14 +117,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in @@ -189,10 +186,9 @@ let vm_conv_gen cv_pb env univs t1 t2 = let v2 = val_of_constr env t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> - (Pp.msg_warning - (Pp.str "Bytecode compilation failed, falling back to default conversion"); - Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) - full_transparent_state env univs t1 t2) + warn_bytecode_compiler_failed (); + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2 let vm_conv cv_pb env t1 t2 = let univs = Environ.universes env in |