8000 Make quotations in terms (e.g. ltac:(), ltac2:(), ...) at the first level of interpretation now strict by default by herbelin · Pull Request #17085 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Make quotations in terms (e.g. ltac:(), ltac2:(), ...) at the first level of interpretation now strict by default #17085

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

Jump to bottom
Closed
wants to merge 2 commits into from
Closed

Make quotations in terms (e.g. ltac:(), ltac2:(), ...) at the first level of interpretation now strict by default #17085

wants to merge 2 commits into from

Conversation

herbelin
Copy link
Member
@herbelin herbelin commented Jan 7, 2023 •
edited
Loading

This was originally in #16935 but #16935 is now split into three parts:

Depends on #16935 (merged) and #17084.

Typical changes of semantics include:

Definition a : forall n : nat, n = n := ltac:(destruct n; auto). (* now fails with n unbound *)
Notation f := ltac:(exact n). (* now fails with n unbound *)
  • Added / updated test-suite.
  • Added changelog.

@herbelin herbelin added part: ltac Issues and PRs related to the Ltac tactic language. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: merge of dependency This PR depends on another PR being merged first. labels Jan 7, 2023
@herbelin herbelin added this to the 8.18+rc1 milestone Jan 7, 2023
@herbelin herbelin requested review from a team as code owners January 7, 2023 17:13
@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 Jan 7, 2023
@herbelin herbelin mentioned this pull request Jan 7, 2023
Merged
1 task
@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 Feb 10, 2023
@coqbot-app
Copy link
Contributor
coqbot-app bot commented Mar 13, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Mar 13, 2023
herbelin added 2 commits March 13, 2023 08:11
@herbelin
Quotations in terms at first level of interpretation are now strict b…
846c74a 
…y default.

This applies to ltac:(), ltac2:(), etc. Examples:
- Definition a : forall n : nat, n = n := ltac:(destruct n; auto).
  now fails because n is unbound in the quotation.
- Notation f := ltac:(exact n).
  now fails at declaration time because n is unbound in the quotation.
@herbelin
Adding change log for rocq-prover#16935.
d353bad
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 17, 2023
@herbelin herbelin force-pushed the master+strict_check-toplevel-ltac-terms branch from 80983e0 to d353bad Compare March 17, 2023 07:58
@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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. labels Mar 17, 2023
@coqbot-app
Copy link
Contributor
coqbot-app bot commented Mar 17, 2023

🔴 CI failure at commit d353bad without any failure in the test-suite

✔️ Corresponding job for the base commit 23b9ea8 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto
  • You can also pass me a specific list of targets to minimize as arguments.

@gares gares modified the milestones: 8.18+rc1, 8.19+rc1 Jul 5, 2023
@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 Nov 15, 2023
@SkySkimmer SkySkimmer removed this from the 8.19+rc1 milestone Nov 22, 2023
@SkySkimmer
Copy link
Contributor

stalled -> removing milestone

@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Dec 15, 2023

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

@coqbot-app coqbot-app bot added the stale This PR will be closed unless it is rebased. label Dec 15, 2023
@coqbot-app coqbot-app
Copy link
Contributor
coqbot-app bot commented Jan 15, 2024

This PR was not rebased after 30 days despite the warning, it is now closed.

@coqbot-app coqbot-app bot closed this Jan 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: merge of dependency This PR depends on another PR being merged first. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: ltac Issues and PRs related to the Ltac tactic language. stale This PR will be closed unless it is rebased.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@herbelin @SkySkimmer @gares
0