diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 18:15:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 18:15:21 +0200 |
| commit | 048b87502eced0a46a654f3f95de8f1968004db1 (patch) | |
| tree | 30adcf8659b4787c80df8b2b9f05cc3fc14715fc /pretyping/vnorm.ml | |
| 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 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 2c6ac7a29..46af784dd 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -316,3 +316,5 @@ let cbv_vm env c t = let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) ~catch_incon:true ~pb env sigma t1 t2 + +let _ = Reductionops.set_vm_infer_conv vm_infer_conv |