Skip to content

Prepare for https://github.com/rocq-prover/stdlib/pull/251 (micromega, tify)#21842

Open
fajb wants to merge 1 commit intorocq-prover:masterfrom
fajb:tify
Open

Prepare for https://github.com/rocq-prover/stdlib/pull/251 (micromega, tify)#21842
fajb wants to merge 1 commit intorocq-prover:masterfrom
fajb:tify

Conversation

@fajb
Copy link
Copy Markdown
Contributor

@fajb fajb commented Mar 30, 2026 •
edited by proux01
Loading

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 30, 2026
SkySkimmer
SkySkimmer reviewed Mar 30, 2026
View reviewed changes
Comment thread plugins/micromega/g_zify.mlg Outdated
let locality = Zify.zify_register_locality

let deprecate_zify_tac zify_tac tify_tac =
CWarnings.create ~name:zify_tac ~category:Deprecation.Version.v9_1
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Mar 30, 2026

Choose a reason for hiding this comment

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

wrong version

Copy link
Copy Markdown
Contributor Author

@fajb fajb Mar 30, 2026

Choose a reason for hiding this comment

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

thanks. Some code was borrowed from a previous (thrashed) PR.

Comment thread plugins/micromega/g_zify.mlg Outdated
(fun () -> Pp.(str "The tactic " ++ str zify_tac ++ str " is deprecated. Use " ++ str tify_tac ++ str " instead."))

let deprecate_zify_vernac cmd1 cmd2 =
CWarnings.create ~name:(cmd1^" Zify "^cmd2) ~category:Deprecation.Version.v9_1
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Mar 30, 2026

Choose a reason for hiding this comment

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

wrong version

@fajb fajb force-pushed the tify branch 2 times, most recently from d33a3fb to 9ec9cd9 Compare March 30, 2026 19:44
@fajb fajb modified the milestone: 9.3+rc1 Mar 30, 2026
@fajb fajb added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic. labels Mar 30, 2026
@fajb
Copy link
Copy Markdown
Contributor Author

fajb commented Mar 30, 2026

@coqbot: run full CI

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 30, 2026
fajb added a commit to fajb/stdlib that referenced this pull request Mar 30, 2026
@fajb
Adapt to rocq-prover/rocq#21842
9a7aa8f 
[zify] Define zify in terms of tify_* tactics
@fajb fajb changed the title [tify] generalise [zify] for an arbitrary type. [tify] generalises [zify] for an arbitrary type. Mar 30, 2026
fajb added a commit to fajb/stdlib that referenced this pull request Mar 31, 2026
@fajb
Adapt to rocq-prover/rocq#21842
3b67e90 
[zify] Define zify in terms of tify_* tactics
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 31, 2026
@fajb
Copy link
Copy Markdown
Contributor Author

fajb commented Mar 31, 2026

@coqbot: run full CI

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 31, 2026
fajb added a commit to fajb/stdlib that referenced this pull request Apr 1, 2026
@fajb
Adapt to rocq-prover/rocq#21842
7253026 
[zify] Define zify in terms of tify_* tactics

restructure components (isolate tify,zify)
@fajb
Copy link
Copy Markdown
Contributor Author

fajb commented Apr 1, 2026

The stdlib should be fixed now.
@coqbot: run full CI

@SkySkimmer SkySkimmer self-assigned this Apr 1, 2026
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 1, 2026
@fajb
Copy link
Copy Markdown
Contributor Author

fajb commented Apr 1, 2026

@coqbot: run full CI

@coqbot-app coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 1, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 2, 2026

If it's ready click ready for review and link the overlay PR in the opening post

@fajb fajb marked this pull request as ready for review April 2, 2026 12:02
@fajb fajb requested review from a team as code owners April 2, 2026 12:02
@fajb
Copy link
Copy Markdown
Contributor Author

fajb commented Apr 2, 2026

If it's ready click ready for review and link the overlay PR in the opening post

Thanks for the reminder

fajb added a commit to fajb/stdlib that referenced this pull request Apr 2, 2026
@fajb
Adapt to rocq-prover/rocq#21842
f57309f 
Just silence the zify warnings.
@coqbot-app coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. 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 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 13, 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 Apr 13, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 14, 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 Apr 14, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 14, 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 Apr 14, 2026
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 14, 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 Apr 14, 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 22, 2026
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

@SkySkimmer SkySkimmer

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: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

3 participants

@fajb @SkySkimmer @proux01