From 1c9bbd7808872b55d55bf7249376f484c9917633 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 1 Apr 2014 17:36:19 +0200 Subject: Propagating conversion_problem towards (postponed) evar/evar problems. Incidentally simplifies where evar/evar problems are treated (in evar_define and imitate rather than solve_simple_eqn). --- pretyping/evarsolve.mli | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'pretyping/evarsolve.mli') diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 28f2fb479..5d0063c47 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -32,14 +32,15 @@ type conv_fun_bool = env -> evar_map -> conv_pb -> constr -> constr -> bool val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> - existential -> constr -> evar_map + bool option -> existential -> constr -> evar_map val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> - existential_key -> constr array -> constr array -> evar_map + bool option -> existential_key -> constr array -> constr array -> evar_map val solve_evar_evar : ?force:bool -> - (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun -> - env -> evar_map -> existential -> existential -> evar_map + (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> + conv_fun -> + env -> evar_map -> bool option -> existential -> existential -> evar_map val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> unification_result -- cgit v1.2.3