From 669dc74d621736d39863e8528b72a33271a6839e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 6 Mar 2023 15:19:15 +0100
Subject: [PATCH] Ltac1 and Ltac2: don't normalize evars for constr:() and
 open_constr:()

Close? #13977
---
 plugins/ltac/tacinterp.ml | 6 +++---
 plugins/ltac2/tac2core.ml | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 595a4e21309c..d605267339bc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -613,7 +613,7 @@ let constr_flags () = {
   use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = true;
-  expand_evars = true;
+  expand_evars = false;
   program_mode = false;
   polymorphic = false;
 }
@@ -632,7 +632,7 @@ let open_constr_use_classes_flags () = {
   use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true;
+  expand_evars = false;
   program_mode = false;
   polymorphic = false;
 }
@@ -642,7 +642,7 @@ let open_constr_no_classes_flags () = {
   use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true;
+  expand_evars = false;
   program_mode = false;
   polymorphic = false;
 }
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index e310ec0421d9..eb2abde67dc7 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -26,7 +26,7 @@ let constr_flags =
     use_typeclasses = Pretyping.UseTC;
     solve_unification_constraints = true;
     fail_evar = true;
-    expand_evars = true;
+    expand_evars = false;
     program_mode = false;
     polymorphic = false;
   }
@@ -38,7 +38,7 @@ let open_constr_no_classes_flags =
   use_typeclasses = Pretyping.NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true;
+  expand_evars = false;
   program_mode = false;
   polymorphic = false;
   }