Merge PR #9062: Delay the computation of frozen evars in legacy unification.

Reviewed-by: mattam82

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;