Commit 2026-07-02 15:44 36d9c9f4

feat(GRewrite): strict rewriting (#38868) This PR makes use of the new grw implementation from #38318, to implement strict rewriting. That is, you can now rewrite with a strict inequality to change the relation in the goal from strict to non-strict. The gcongr and grw tactics now look up slightly differently in the gcongrExt environment extension, because gcongr knows the constant on both sides of the relation, while grw knows it on only one side. It would be possible to have two separate dictionaries in the environment for these two use cases. However, I have implemented it with just a single dictionary in the environment, as this reduces the overhead of having the environment extension. Note: in order to make strict rewriting have priority over the old behaviour, lt_of_lt_of_le and lt_of_lt_of_le' need to be preferred over le_imp_le_of_le_of_le and lt_imp_lt_of_le_of_le. Luckily this is the case because the former have fewer varying arguments than the latter. So, we don't need to explicitly set a high priority.