Skip to content
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

Add Ltac2.Constr.{is_float,is_uint63,is_array} #17894

Merged
merged 1 commit into from Aug 1, 2023
Merged

Add Ltac2.Constr.{is_float,is_uint63,is_array} #17894

merged 1 commit into from Aug 1, 2023

Conversation

JasonGross
Copy link
Member

@JasonGross JasonGross commented Jul 26, 2023 •
edited

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Updated documented syntax by running make doc_gram_rsts.

@JasonGross JasonGross added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Jul 26, 2023
@JasonGross JasonGross requested a review from a team as a code owner July 26, 2023 20:16
@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 Jul 26, 2023
@SkySkimmer SkySkimmer 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 Jul 31, 2023
@SkySkimmer SkySkimmer self-assigned this Jul 31, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Jul 31, 2023
@SkySkimmer
Copy link
Contributor

@coqbot run full ci

@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 74e210c into coq:master Aug 1, 2023
7 checks passed
@JasonGross JasonGross deleted the is_float branch August 1, 2023 18:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@JasonGross @SkySkimmer @ppedrot