diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /pretyping/evarconv.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'pretyping/evarconv.mli')
-rw-r--r-- | pretyping/evarconv.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 9270d6e3..cdf5dd0e 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -28,7 +28,13 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma (** The same function resolving evars by side-effect and catching the exception *) val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.conv]"] + val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool +[@@ocaml.deprecated "Use [Evarconv.cumul]"] + +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option (** {6 Unification heuristics. } *) @@ -63,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map -> (** Declare function to enforce evars resolution by using typing constraints *) -val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit +val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result |