diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-29 16:04:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | 84290ba5da2a6acb4bf95b197f7a7ce8b072a1d0 (patch) | |
| tree | 61c59f4149978e84ccf77b78ecb70ce3e3dd2188 /pretyping/evarsolve.mli | |
| parent | 902da7d2949464ff54dafc3fda1d44365270d2e1 (diff) | |
Find a more efficient fix for dealing with template universes:
eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index ca03f9853..23ed6a2ef 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -35,6 +35,7 @@ val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?all:bool (* Include domains of products *) -> + ?template:bool -> (* Generate template fresh universe variables, to be instantiated eagerly *) ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> |