diff options
| -rw-r--r-- | kernel/reduction.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 7 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.mli | 4 |
6 files changed, 17 insertions, 5 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c2ab22e99..c1f0008e6 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 = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f6c186728..d484df69c 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 d25e273a3..bb1bc7d2e 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 42c2c9c6e..d5a844847 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 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 diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 99856a8d9..9421b2d85 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 |