From fea073c74f98f3fe6728363c0f8142520ac1e50c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 14:42:01 +0200
Subject: Replace `frozen` by `allowed` evars in evarconv, and delay them

This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fb149071c9..a8a3a21f4a 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.allowed_evars = Unification.AllowAll;
+  Unification.allowed_evars = Evarsolve.AllowAll;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
-- 
cgit v1.2.3


From cd37a10f9cf5746edf16611d7f833e0e8cf2c5f8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 18:10:37 +0200
Subject: Abstract type for allowed evars

---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a8a3a21f4a..a1dbf9a439 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.allowed_evars = Evarsolve.AllowAll;
+  Unification.allowed_evars = Evarsolve.AllowedEvars.all;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
-- 
cgit v1.2.3