Commit 2024-09-12 01:45 b9bbf9b8
View on Github →chore: namespace rsuffices (#16708)
rsuffices should be globally available as a tactic, but having it available as an un-namespaced term of type ParserDescr is silly.
chore: namespace rsuffices (#16708)
rsuffices should be globally available as a tactic, but having it available as an un-namespaced term of type ParserDescr is silly.