From 122a5aca4f7b21f65afece2c59e8529183713d71 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 27 Apr 2018 20:52:36 +0200
Subject: 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.
---
 proofs/clenvtac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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;
-- 
cgit v1.2.3