From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 kernel/nativeconv.ml | 19 +++++--------------
 1 file changed, 5 insertions(+), 14 deletions(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 2a7afdca..c75dde84 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu =
     match a1, a2 with
     | Ameta (m1,_), Ameta (m2,_) ->
       if Int.equal m1 m2 then cu else raise NotConvertible
-    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+    | Aevar (ev1, args1), Aevar (ev2, args2) ->
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
@@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu =
        let cu = conv_val env CONV lvl d1 d2 cu in
        let v = mk_rel_accu lvl in
        conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
-    | Aproj(p1,ac1), Aproj(p2,ac2) ->
-       if not (Constant.equal p1 p2) then raise NotConvertible
+    | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) ->
+       if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
        else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
@@ -141,23 +141,14 @@ let warn_no_native_compiler =
          (fun () -> strbrk "Native compiler is disabled," ++
                       strbrk " falling back to VM conversion test.")
 
-type vm_conv_gen = { vm_conv_gen : 'a. conv_pb -> (Constr.types, 'a) generic_conversion_function }
-
-let vm_conv_gen =
-  ref { vm_conv_gen = fun cv_pb env univs t1 t2 ->
-    generic_conv cv_pb ~l2r:false (fun _ -> None) full_transparent_state env univs t1 t2 }
-
-let set_vm_conv_gen f = vm_conv_gen := f
-
 let native_conv_gen pb sigma env univs t1 t2 =
   if not Coq_config.native_compiler then begin
     warn_no_native_compiler ();
-    vm_conv_gen.contents.vm_conv_gen pb env univs t1 t2
+    Vconv.vm_conv_gen pb env univs t1 t2
   end
   else
-  let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
-  let code, upds = mk_conv_code penv sigma prefix t1 t2 in
+  let code, upds = mk_conv_code env sigma prefix t1 t2 in
   match compile ml_filename code ~profile:false with
   | (true, fn) ->
       begin
-- 
cgit v1.2.3