diff options
Diffstat (limited to 'pretyping/evarconv.mli')
-rw-r--r-- | pretyping/evarconv.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 627430708..cdf5dd0e5 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. } *) @@ -38,7 +44,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map -(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) +[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"] (** Check all pending unification problems are solved and raise an error otherwise *) @@ -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 |