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

extensionality tactic is missing in the manual #19948

Open
yaitskov opened this issue Dec 17, 2024 · 1 comment
Open

extensionality tactic is missing in the manual #19948

yaitskov opened this issue Dec 17, 2024 · 1 comment
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: documentation Additions or improvement to documentation.

Comments

@yaitskov
Copy link
Contributor

Description of the problem

Rocq manual changelog mentions that the extensionality tactic is added, but there is no section for such tactic and the name is not in the index.

Small Rocq / Coq file to reproduce the bug

No response

Version of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response
@yaitskov yaitskov added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Dec 17, 2024
@SkySkimmer
Copy link
Contributor

I guess it means

coq/stdlib/theories/Logic/FunctionalExtensionality.v

Lines 159 to 174 in e1eeac5

Tactic Notation "extensionality" ident(x) :=
match goal with
[ |- ?X = ?Y ] =>
(apply (@functional_extensionality _ _ X Y) ||
apply (@functional_extensionality_dep _ _ X Y) ||
apply forall_extensionalityP ||
apply forall_extensionalityS ||
apply forall_extensionality) ; intro x
end.
(** Iteratively apply [functional_extensionality] on an hypothesis
until finding an equality statement *)
(* Note that you can write [Ltac extensionality_in_checker tac ::= tac tt.] to get a more informative error message. *)
Ltac extensionality_in_checker tac :=
first [ tac tt | fail 1 "Anomaly: Unexpected error in extensionality tactic. Please report." ].
Tactic Notation "extensionality" "in" hyp(H) :=

@SkySkimmer SkySkimmer added kind: documentation Additions or improvement to documentation. and removed needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Dec 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: documentation Additions or improvement to documentation.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@yaitskov @SkySkimmer