From 9a026fcaeb3fa2678b9c93da8204f9f1ddcc0b31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Sep 2020 09:54:42 +0200
Subject: Remove the compare_graph field from the conversion API.

We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.
---
 kernel/nativeconv.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/nativeconv.ml')

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 01e9550ec5..3543168175 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 univs t1 t2 =
+let native_conv_gen pb sigma env graph univs t1 t2 =
   if not (typing_flags env).Declarations.enable_native_compiler then begin
     warn_no_native_compiler ();
-    Vconv.vm_conv_gen pb env univs t1 t2
+    Vconv.vm_conv_gen pb env graph univs t1 t2
   end
   else
   let ml_filename, prefix = get_ml_filename () in
@@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 =
     else Constr.eq_constr_univs univs t1 t2
   in
   if not b then
-    let univs = (univs, checked_universes) in
+    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 t1 t2 in ()
+    let _ = native_conv_gen cv_pb sigma env univs state t1 t2 in ()
-- 
cgit v1.2.3


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