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

Close? #13977 Unlike #17346 we still expand in `constr:()`, hopefully we trigger less bugs this way.
coq · Oct 16, 2023 · 2207de7 · 2207de7
1 parent 49fce3a
commit 2207de7
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/doc/changelog/04-tactics/17704-open-constr-no-expand.rst b/doc/changelog/04-tactics/17704-open-constr-no-expand.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  `open_constr` in Ltac1 and Ltac2 does not perform evar normalization.
+  Normalization may be recovered using `let c := open_constr:(...) in constr:(c)`
+  if necessary for performance
+  (`#17704 <https://github.com/coq/coq/pull/17704>`_,
+  by Gaëtan Gilbert).
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
@@ -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
@@ -39,7 +39,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;
   }