diff options
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 094dae4828..d347f46637 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -136,6 +136,24 @@ val solve_evar_evar : ?force:bool -> (** The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised *) +(* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)] + makes progresses on problems of the form [?ev[inst] := t] (or + [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a + limited form of projection. At the time of writing this comment, + only rels/vars (possibly indirectly via a chain of evars) and + constructors are used for projection. For instance + [?e[x,S 0] := x + S 0] will be solved by imitating [+] and + projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in + [?e[0+0] := 0+0], the possible imitation will not be seen. + + [choose] tells to make an irreversible choice when two valid + projections are competing. It is to be used when no more reversible + progress can be done. It is [false] by default. + + [imitate_defs] tells to expand local definitions if they cannot be + projected. It is [true] by default. +*) + val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result |