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.ml | |
| 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.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 16a044528..8f696b84c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -26,7 +26,7 @@ let normalize_evar evd ev = | Evar (evk,args) -> (evk,args) | _ -> assert false -let refresh_universes ?(all=false) ?(with_globals=false) dir evd t = +let refresh_universes ?(all=false) ?(template=false) ?(with_globals=false) dir evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = match kind_of_term t with @@ -34,7 +34,7 @@ let refresh_universes ?(all=false) ?(with_globals=false) dir evd t = || (with_globals && Evd.is_sort_variable evd s = None) -> (modified := true; (* s' will appear in the term, it can't be algebraic *) - let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in + let s' = evd_comb0 (new_sort_variable ~template Evd.univ_flexible) evdref in evdref := (if dir then set_leq_sort !evdref s' s else set_leq_sort !evdref s s'); |