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

In "intro y" on a goal statement which is an existential variable, use the name "y" in the context of all resulting goals #18395

Merged
merged 2 commits into from Jan 8, 2024
Merged

In "intro y" on a goal statement which is an existential variable, use the name "y" in the context of all resulting goals #18395

merged 2 commits into from Jan 8, 2024

Conversation

herbelin
Copy link
Member

Calling intro y on an evar ?A forces the evar to be a defined as a forall x : ?T, ?P. The PR ensures that the internal name of the product is the same as the one used in the introduction. Here is an example:

Goal exists (A:Prop), A.
eexists.
unshelve intro y.
(* before the PR:  |- ?T : Type    x : ?T |- ?P : Prop     y : ?T |- ?Goal : ?P *)
(* after the PR:   |- ?T : Type    y : ?T |- ?P : Prop     y : ?T |- ?Goal : ?P *)
  • Added / updated test-suite (there was an existing intro x example working by chance because the default variable name was precisely x)

@herbelin herbelin added part: tactics kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: existential variables Existential variables, also known as evars, represent as yet unknown values in a proof. request: full CI Use this label when you want your next push to trigger a full CI. labels Dec 10, 2023
@herbelin herbelin added this to the 8.20+rc1 milestone Dec 10, 2023
@herbelin herbelin requested review from a team as code owners December 10, 2023 08:07
@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 Dec 10, 2023
@ppedrot ppedrot added the needs: overlay This is breaking external developments we track in CI. label Dec 10, 2023
ppedrot
ppedrot reviewed Dec 10, 2023
View reviewed changes
pretyping/evardefine.mli Outdated Show resolved Hide resolved
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 10, 2023
@herbelin herbelin force-pushed the master+use-intro-name-in-evar-context-when-goal-is-evar branch from 8e69dfb to 63da26a Compare December 10, 2023 12:03
@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 Dec 10, 2023
@ppedrot ppedrot self-assigned this Dec 10, 2023
@herbelin herbelin removed the needs: overlay This is breaking external developments we track in CI. label Dec 10, 2023
@ppedrot
Copy link
Member

ppedrot commented Dec 18, 2023

@herbelin this probably deserves a changelog, on second thought.

@ppedrot ppedrot added the needs: changelog entry This should be documented in doc/changelog. label Dec 29, 2023
@ppedrot
Copy link
Member

ppedrot commented Jan 5, 2024

@herbelin ping, this just needs a trivial changelog.

herbelin added a commit to herbelin/github-coq that referenced this pull request Jan 5, 2024
@herbelin
Change log for coq#18395
fe662a6
@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 5, 2024
@herbelin
Copy link
Member Author

herbelin commented Jan 5, 2024

I tried to write some change log lines...

ppedrot
ppedrot reviewed Jan 7, 2024
View reviewed changes
doc/changelog/04-tactics/18395-master+use-intro-name-in-evar-context-when-goal-is-evar.rst Outdated
@@ -0,0 +1,10 @@
- **Changed:**
:tac:`intro z` on an existential variable goal forces the resolution
Copy link
Member

@ppedrot ppedrot Jan 7, 2024 •
edited

Choose a reason for hiding this comment

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

:tac: doesn't seem to be a proper tag. Since it's not a tactic reference either I think you can just write intro z (within quotes I don't know how to escape in markdown syntax).

Copy link
Member Author

Choose a reason for hiding this comment

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

OK, I made another try.

@herbelin herbelin force-pushed the master+use-intro-name-in-evar-context-when-goal-is-evar branch from fe662a6 to 17798c8 Compare January 7, 2024 16:24
@ppedrot
Copy link
Member

ppedrot commented Jan 8, 2024

@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 Jan 8, 2024
@ppedrot ppedrot removed the needs: changelog entry This should be documented in doc/changelog. label Jan 8, 2024
@ppedrot
Copy link
Member

ppedrot commented Jan 8, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit fa3c613 into coq:master Jan 8, 2024
5 of 7 checks passed
louiseddp pushed a commit to louiseddp/coq that referenced this pull request Feb 27, 2024
@herbelin @louiseddp
Change log for coq#18395
8c2e30f
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

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: existential variables Existential variables, also known as evars, represent as yet unknown values in a proof. part: tactics
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@herbelin @ppedrot