From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 kernel/vconv.ml | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

(limited to 'kernel/vconv.ml')

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
-- 
cgit v1.2.3