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.

5 files changed, 16 insertions, 5 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f6c1867285..d484df69c1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,7 +929,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
-		let (evd,b) = Vnorm.vm_infer_conv env !evdref cty tval in
+		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
 		if b then (evdref := evd; cj)
 		else
 		  error_actual_type_loc loc env !evdref cj tval 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d25e273a3e..bb1bc7d2ea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1321,6 +1321,12 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
 let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
       Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
 
+(* This reference avoids always having to link C code with the kernel *)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state)
+let set_vm_infer_conv f = vm_infer_conv := f
+let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
+  !vm_infer_conv ~pb env t1 t2
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 42c2c9c6e6..d5a844847c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -272,6 +272,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
   env -> evar_map -> constr -> constr -> evar_map * bool
 
+(** Conversion with inference of universe constraints *)
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool) -> unit
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
+
+
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
 conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2c6ac7a292..46af784dda 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
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 99856a8d9a..9421b2d859 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -12,7 +12,3 @@ open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
-
-(** Conversion with inference of universe constraints *)
-val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool