Ltac1 and Ltac2: don't normalize evars for constr:() and open_constr:()

Close? coq#13977
SkySkimmer · Oct 10, 2023 · 669dc74 · 669dc74
1 parent 179fbdd
commit 669dc74
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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;
   }