diff options
| author | Maxime Dénès | 2015-10-15 18:15:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-15 18:15:21 +0200 |
| commit | 048b87502eced0a46a654f3f95de8f1968004db1 (patch) | |
| tree | 30adcf8659b4787c80df8b2b9f05cc3fc14715fc /kernel | |
| parent | ba8dd1c47bcbbcd2678eca78783db7f5c95f37e7 (diff) | |
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.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 = |