diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-01 17:36:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-01 18:47:54 +0200 |
| commit | 1c9bbd7808872b55d55bf7249376f484c9917633 (patch) | |
| tree | f21a44463b3957a5f2529cb2dea526a8f92db662 /pretyping/evarsolve.mli | |
| parent | 36dd5dba9c7a86ef97e9f8bd96cbf6340098e2b7 (diff) | |
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).
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 9 |
1 files changed, 5 insertions, 4 deletions
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 |