diff options
| author | Pierre-Marie Pédrot | 2018-04-27 20:52:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-17 13:39:16 +0200 |
| commit | 122a5aca4f7b21f65afece2c59e8529183713d71 (patch) | |
| tree | b32219ae0d559fbe60d1319d4cb8b3088b238c44 /plugins | |
| parent | 354ac6a0c59f77d8a7d63c84144c044fe958fa3c (diff) | |
Delay the computation of frozen evars in legacy unification.
This source of slowness has been observed in VST, but it is probably
pervasive. Most of the unification problems are not mentioning evars,
it is thus useless to compute the set of frozen evars upfront.
We also seize the opportunity to reverse the flag, because it is always
used negatively.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 726752a2bf..1493092f2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = Evar.Set.empty; + Unification.allowed_evars = Unification.AllowAll; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; |