From 2207de7a2235910c1f7158bbbb15b39a9f2bc029 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 6 Mar 2023 15:19:15 +0100 Subject: [PATCH] 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. --- doc/changelog/04-tactics/17704-open-constr-no-expand.rst | 6 ++++++ plugins/ltac/tacinterp.ml | 4 ++-- plugins/ltac2/tac2core.ml | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/04-tactics/17704-open-constr-no-expand.rst 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; }