Skip to content

[ssreflect] Use rw instead of rewrite to avoid conflicts with legacy tactic #21478

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 11 commits into from
Apr 1, 2026
Merged

[ssreflect] Use rw instead of rewrite to avoid conflicts with legacy tactic #21478

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
2df15a2
Update comment
proux01 Mar 17, 2026
3225945
[ssreflect] Cleanup old vim vars
proux01 Jan 7, 2026
8a048a1
[ssreflect] Cleanup old compat code
proux01 Mar 19, 2026
db2107c
[ssreflect] Update outdated comment
proux01 Mar 19, 2026
139adb2
[ssreflect] Use ‗ instead of _ for reserved identifiers
proux01 Mar 19, 2026
3d59417
[ssreflect] Rename SSR Loaded to SSRRewriteLoaded
proux01 Mar 19, 2026
3d24d7a
[ssreflect] Use tactic name 'rw' instead of 'rewrite'
proux01 Mar 20, 2026
9e9afe1
[ssreflect] Renaming rewrite -> rw
proux01 Mar 20, 2026
c4a7ced
[ssreflect] Deprecate rewrite
proux01 Mar 20, 2026
90ad540
Update doc
proux01 Mar 20, 2026
72cca58
Add changelog
proux01 Mar 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions clib/unicode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,7 @@ let classify =
mk_lookup_table_from_unicode_tables_for IdentSep
[
single 0x005F; (* Underscore. *)
single 0x2017; (* Double low line. *)
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why?

Copy link
Copy Markdown
Contributor Author

@proux01 proux01 Feb 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ssreflect was using _foo_ for reserved identifiers (the ones introduced by move=> ?) which forbids explicitly using any such identifier. To avoid conflicts this changes it to ‗foo‗.

single 0x00A0; (* Non breaking space, overrides Sep *)
];
mk_lookup_table_from_unicode_tables_for IdentPart
Expand Down
2 changes: 1 addition & 1 deletion doc/Makefile.docgram
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ REAL_DOC_MLGS := $(wildcard */*.mlg plugins/*/*.mlg)
# omit SSR MLGS and chapter for now
SSR_MLGS := \
plugins/ssr/ssrparser.mlg plugins/ssr/ssrtacs.mlg plugins/ssr/ssrvernac.mlg \
plugins/ssrmatching/g_ssrmatching.mlg
plugins/ssrmatching/g_ssrmatching.mlg plugins/ssrrewrite/ssrrewrite.mlg
REAL_DOC_MLGS := $(filter-out $(SSR_MLGS),$(REAL_DOC_MLGS))
SSR_RSTS := doc/sphinx/proof-engine/ssreflect-proof-language.rst
DOC_RSTS := $(filter-out $(SSR_RSTS),$(DOC_RSTS))
Expand Down
12 changes: 12 additions & 0 deletions doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
- **Changed:**
``rewrite`` tactic for ``rw``. Since this was the major cause of
conflict with legacy tactics, ssreflect can now be loaded with less
conflicts through ``From Corelib Require Import ssreflect_rw.``.
For backward compatibility
``From Corelib Require Import ssreflect.``
still loads a ``rewrite`` wrapper to ``rw`` as well as the
``if <term> is <pattern> then <term> else <term>``
and ``if <term> isn't <pattern> then <term> else <term>``
syntactic sugars for match
(`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
by Pierre Roux).
1 change: 1 addition & 0 deletions doc/corelib/index-list.html.template
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,7 @@ through the <tt>Require Import</tt> command.</p>
<dd>
theories/Corelib/ssrmatching/ssrmatching.v
theories/Corelib/ssr/ssrclasses.v
theories/Corelib/ssr/ssreflect_rw.v
theories/Corelib/ssr/ssreflect.v
theories/Corelib/ssr/ssrbool.v
theories/Corelib/ssr/ssrfun.v
Expand Down
2 changes: 1 addition & 1 deletion doc/sphinx/addendum/generalized-rewriting.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -484,7 +484,7 @@ It is used in two cases:
constraint can be automatically discharged.

+ Compatibility with ssreflect's rewrite:
The :tacn:`rewrite (ssreflect)` tactic uses generalized rewriting when possible, by
The :tacn:`rw` tactic uses generalized rewriting when possible, by
checking that a ``RewriteRelation R`` instance exists when rewriting with a
term of type ``R t u``.

Expand Down
4 changes: 2 additions & 2 deletions doc/sphinx/changes.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10079,7 +10079,7 @@ Changes in 8.11+beta1
relation. More precisely, assume the given context lemma has type
`forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The
first step performed by :tacn:`under` (since Coq 8.10) amounts to
calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which
calling the tactic :tacn:`rw`, which
itself relies on :tacn:`setoid_rewrite` if need be. So this step was
already compatible with a double implication or setoid equality for
the conclusion head symbol `R2`. But a further step consists in
Expand Down Expand Up @@ -11109,7 +11109,7 @@ Many bug fixes and documentation improvements, in particular:
by Andreas Lynge, review by Enrico Tassi)
- Make the ``rewrite /t`` tactic work together with
:flag:`Universe Polymorphism`.
This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT
This makes :tacn:`rw` compatible with the HoTT
library https://github.com/HoTT/HoTT
(`#10305 <https://github.com/rocq-prover/rocq/pull/10305>`_,
fixes `#9336 <https://github.com/rocq-prover/rocq/issues/9336>`_,
Expand Down
Loading
Loading