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 /pretyping/reductionops.mli | |
| 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/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
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 -> |