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/vconv.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cc2c2c0b4b..304e7e8470 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -190,10 +190,10 @@ let warn_bytecode_compiler_failed =
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 
-let vm_conv_gen cv_pb env univs t1 t2 =
+let vm_conv_gen cv_pb env graph univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env univs t1 t2
+      TransparentState.full env graph univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -202,7 +202,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env univs t1 t2
+      TransparentState.full env graph univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
@@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 =
     else Constr.eq_constr_univs univs t1 t2
   in
   if not b then
-    let univs = (univs, checked_universes) in
-    let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+    let state = (univs, checked_universes) in
+    let _ = vm_conv_gen cv_pb 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/vconv.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/vconv.ml')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 304e7e8470..948195797e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -190,10 +190,10 @@ let warn_bytecode_compiler_failed =
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 
-let vm_conv_gen cv_pb env graph univs t1 t2 =
+let vm_conv_gen cv_pb env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env graph univs t1 t2
+      TransparentState.full env univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -202,7 +202,7 @@ let vm_conv_gen cv_pb env graph univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env graph univs t1 t2
+      TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
@@ -212,4 +212,4 @@ let vm_conv cv_pb env t1 t2 =
   in
   if not b then
     let state = (univs, checked_universes) in
-    let _ = vm_conv_gen cv_pb env univs state t1 t2 in ()
+    let _ = vm_conv_gen cv_pb env state t1 t2 in ()
-- 
cgit v1.2.3