From 048b87502eced0a46a654f3f95de8f1968004db1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2015 18:15:21 +0200
Subject: Avoid dependency of the pretyper on C code.

Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.

This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
---
 kernel/reduction.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c2ab22e995..c1f0008e63 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -716,6 +716,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
+(* This reference avoids always having to link C code with the kernel *)
 let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
-- 
cgit v1.2.3