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

ltac2val:() quotation in ltac1 to return Ltac1.t values #17575

Merged
merged 2 commits into from Jun 1, 2023
Merged

ltac2val:() quotation in ltac1 to return Ltac1.t values #17575

merged 2 commits into from Jun 1, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented May 5, 2023 •
edited

This allows returning values from ltac2 to ltac1

Overlays:

@SkySkimmer SkySkimmer added needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. labels May 5, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner May 5, 2023 14:08
@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 May 5, 2023
ppedrot
ppedrot reviewed May 5, 2023
View reviewed changes
plugins/ltac2/tac2intern.ml Outdated Show resolved Hide resolved
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. and removed needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels May 9, 2023
@SkySkimmer SkySkimmer changed the title ltac2:() in ltac1 with no binders and at type Ltac1.t does not drop the value ltac2val:() in ltac1 with no binders and at type Ltac1.t does not drop the value May 9, 2023
@SkySkimmer SkySkimmer changed the title ltac2val:() in ltac1 with no binders and at type Ltac1.t does not drop the value ltac2val:() in ltac1 with no binders and at type Ltac1.t returns the value May 9, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner May 9, 2023 16:01
@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 May 9, 2023
@SkySkimmer SkySkimmer changed the title ltac2val:() in ltac1 with no binders and at type Ltac1.t returns the value ltac2val:() quotation in ltac1 to return Ltac1.t values May 9, 2023
jfehrle
jfehrle reviewed May 9, 2023
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

Some suggestions

doc/sphinx/proof-engine/ltac2.rst Show resolved Hide resolved
doc/sphinx/proof-engine/ltac2.rst Show resolved Hide resolved
doc/changelog/06-Ltac2-language/17575-ltac2in1.rst Outdated Show resolved Hide resolved
doc/sphinx/proof-engine/ltac2.rst Outdated Show resolved Hide resolved
@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 May 10, 2023
@SkySkimmer SkySkimmer added needs: progress Work in progress: awaiting action from the author. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels May 10, 2023
@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 May 10, 2023
@ppedrot ppedrot self-assigned this May 11, 2023
SkySkimmer added a commit to SkySkimmer/coq-serapi that referenced this pull request May 17, 2023
@SkySkimmer
Adapt to coq/coq#17575 (ltac2val in ltac1)
aa5494a
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 17, 2023
@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 May 17, 2023
@SkySkimmer SkySkimmer added this to the 8.18+rc1 milestone May 22, 2023
ppedrot
ppedrot reviewed May 23, 2023
View reviewed changes
plugins/ltac2/tac2env.ml Outdated
@@ -308,11 +308,23 @@ let ltac1_prefix =

(** Generic arguments *)

let wit_ltac2 = Genarg.make0 "ltac2:tactic"
let wit_ltac2_val = Genarg.make0 "ltac2:value"
module Ltac2in1 = struct
Copy link
Member

Choose a reason for hiding this comment

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

This should probably go into Tac2expr instead, and also I'm not a huge fan of the module wrapper.

Copy link
Member

Choose a reason for hiding this comment

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

Ping @SkySkimmer

Copy link
Contributor Author

Choose a reason for hiding this comment

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

changed

SkySkimmer added a commit to SkySkimmer/coq-serapi that referenced this pull request May 30, 2023
@SkySkimmer
Adapt to coq/coq#17575 (ltac2val in ltac1)
94447f9
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 30, 2023
@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 May 30, 2023
@SkySkimmer SkySkimmer requested a review from a team May 31, 2023 10:09
@ppedrot
Copy link
Member

ppedrot commented Jun 1, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 8967d5b into coq:master Jun 1, 2023
12 checks passed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 1, 2023

@ppedrot: Please take care of the following overlays:

  • 17575-SkySkimmer-ltac2in1.sh

ppedrot added a commit to ejgallego/coq-serapi that referenced this pull request Jun 1, 2023
@ppedrot
Merge pull request #333 from SkySkimmer/ltac2in1
5b11174 
Adapt to coq/coq#17575 (ltac2val in ltac1)
@SkySkimmer SkySkimmer deleted the ltac2in1 branch June 2, 2023 10:08
@SkySkimmer SkySkimmer mentioned this pull request Oct 3, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@RalfJung RalfJung RalfJung left review comments

@jfehrle jfehrle jfehrle left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@SkySkimmer @ppedrot @RalfJung @jfehrle