From eb5a67de1fc586acc588d5c61c84df670284f054 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2020 17:40:01 +0200
Subject: Pick the universe graph out of the environment in conversion API.

---
 kernel/nativeconv.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3543168175..fc6afb79d4 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -150,10 +150,10 @@ let warn_no_native_compiler =
          (fun () -> strbrk "Native compiler is disabled," ++
                       strbrk " falling back to VM conversion test.")
 
-let native_conv_gen pb sigma env graph univs t1 t2 =
+let native_conv_gen pb sigma env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_native_compiler then begin
     warn_no_native_compiler ();
-    Vconv.vm_conv_gen pb env graph univs t1 t2
+    Vconv.vm_conv_gen pb env univs t1 t2
   end
   else
   let ml_filename, prefix = get_ml_filename () in
@@ -179,4 +179,4 @@ let native_conv cv_pb sigma env t1 t2 =
     let state = (univs, checked_universes) in
     let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
     let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
-    let _ = native_conv_gen cv_pb sigma env univs state t1 t2 in ()
+    let _ = native_conv_gen cv_pb sigma env state t1 t2 in ()
-- 
cgit v1.2.3