From 0f74b3df6e64dc069e53c4afcd6f46129b211d09 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Oct 2015 13:50:55 +0200
Subject: Remove reference to default conversion function inside the kernel.

---
 kernel/reduction.ml  | 7 +------
 kernel/reduction.mli | 1 -
 2 files changed, 1 insertion(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b09367dd92..68783780d3 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -738,14 +738,9 @@ let vm_conv cv_pb env t1 t2 =
       (* If compilation fails, fall-back to closure conversion *)
       fconv cv_pb false (fun _->None) env t1 t2
 
-
-let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
-
-let set_default_conv f = default_conv := f
-
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
   try
-    !default_conv ~l2r cv_pb env t1 t2
+    fconv cv_pb l2r (fun _ -> None) env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
       fconv cv_pb false (fun _->None) env t1 t2
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ced5c4985..90c008b19d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -93,7 +93,6 @@ val set_nat_conv :
   (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
 val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
 
-val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
 val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
 val default_conv_leq : ?l2r:bool -> types conversion_function
 
-- 
cgit v1.2.3