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.

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 1904d9b112..8e7d1df29a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -108,7 +108,7 @@ let fail_quick_core_unif_flags = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  frozen_evars = Evar.Set.empty;
+  allowed_evars = AllowAll;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;