Skip to content

Add ssreflect to the prelude#21776

Draft
proux01 wants to merge 4 commits into
rocq-prover:masterfrom
proux01:ssreflect-prelude
Draft

Add ssreflect to the prelude#21776
proux01 wants to merge 4 commits into
rocq-prover:masterfrom
proux01:ssreflect-prelude

Conversation

@proux01
Copy link
Copy Markdown
Contributor

@proux01 proux01 commented Mar 18, 2026 •
edited
Loading

This adds ssreflect to the prelude (split out of #21478)

Depends on: #21478 (merged)

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

@proux01 proux01 added needs: discussion Further discussion is needed. part: ssreflect The SSReflect proof language. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. request: full CI Use this label when you want your next push to trigger a full CI. part: core library Corelib in theories/ labels Mar 18, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from b3eaab4 to 56b6739 Compare March 18, 2026 13:51
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2026
@proux01 proux01 mentioned this pull request Mar 18, 2026
Merged
5 tasks
@proux01 proux01 added the needs: merge of dependency This PR depends on another PR being merged first. label Mar 18, 2026
@proux01 proux01 added this to the 9.3+rc1 milestone Mar 18, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from 56b6739 to 7230912 Compare March 18, 2026 14:56
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 19, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from 7230912 to 998f839 Compare March 19, 2026 17:49
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 19, 2026
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 20, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from 998f839 to 6318b5c Compare March 27, 2026 10:21
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Mar 27, 2026
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 1, 2026
@proux01 proux01 added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: merge of dependency This PR depends on another PR being merged first. labels Apr 1, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from 6318b5c to 66244a8 Compare April 1, 2026 06:58
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@coqbot-app coqbot-app Bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 1, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 6, 2026
@proux01 proux01 force-pushed the ssreflect-prelude branch from 66244a8 to f51504d Compare April 6, 2026 14:53
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 6, 2026
@github-actions github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 21, 2026
SkySkimmer
SkySkimmer reviewed Apr 28, 2026
View reviewed changes
Comment thread test-suite/Makefile
export LC_CTYPE=C; \
export LANG=C; \
$(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" -norec $(shell basename $< .v) > $$output 2>&1) ; \
$(call WITH_TIMER,$(patsubst %.v.log,%.chk.log,$@),$(coqchk) -o -silent $(call get_coqchk_prog_args,"$<") -Q $(shell dirname $<) "" $(shell basename $< .v) > $$output 2>&1) ; \
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Apr 28, 2026

Choose a reason for hiding this comment

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

???

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: discussion Further discussion is needed. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: core library Corelib in theories/ part: ssreflect The SSReflect proof language.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@proux01 @SkySkimmer