diff options
| author | Matthieu Sozeau | 2018-10-17 19:24:30 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:20:07 +0100 |
| commit | e3178fb2de9a84bbcdc90a60cd8f27cd1323eb36 (patch) | |
| tree | e09126eee58e09c7b640e1440cc93b98b9781646 /pretyping/evarsolve.mli | |
| parent | 93ef4e058cb9f7bfc6f3abc8bdc5752a2d8df5ca (diff) | |
Document the unify_flags more throroughly in evarsolve.
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index dfadb4aaea..ce803fe254 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -18,12 +18,22 @@ val of_alias : alias -> EConstr.t type unify_flags = { modulo_betaiota : bool; + (* Enable beta-iota reductions during unification *) open_ts : Names.transparent_state; + (* Enable delta reduction according to open_ts for open terms *) closed_ts : Names.transparent_state; + (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *) subterm_ts : Names.transparent_state; + (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order + unifications. *) frozen_evars : Evar.Set.t; + (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *) allow_K_at_toplevel : bool; - with_cs : bool} + (* During higher-order unifications, allow to produce K-redexes: i.e. to produce + an abstraction for an unused argument *) + with_cs : bool + (* Enable canonical structure resolution during unification *) +} type unification_result = | Success of evar_map |