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

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).

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;
 }

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;
   }