diff --git a/doc/changelog/04-tactics/17704-open-constr-no-expand.rst b/doc/changelog/04-tactics/17704-open-constr-no-expand.rst new file mode 100644 index 000000000000..de4482c988f5 --- /dev/null +++ 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 `_, + by Gaƫtan Gilbert). diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 595a4e21309c..b1b05e4a7e6f 100644 --- 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 index d70a4daac55a..478676239dcd 100644 --- 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; }