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

Ltac2 should support deprecated attributes #12317

Closed
JasonGross opened this issue May 13, 2020 · 0 comments · Fixed by #13774
Closed

Ltac2 should support deprecated attributes #12317

JasonGross opened this issue May 13, 2020 · 0 comments · Fixed by #13774
Labels
part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2
Milestone
8.14+rc1

Comments

@JasonGross
Copy link
Member

Description of the problem

#[deprecated(since="8.12",note="Use Constr.Case.make instead.")]
Ltac2 @ external case : inductive -> case := "ltac2" "constr_case".
(** Generate the case information for a given inductive type. *)

gives

Error: This command does not support this attribute: deprecated.
[unsupported-attributes,parsing]

Coq Version

master
@JasonGross JasonGross added the part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. label May 13, 2020
@JasonGross JasonGross mentioned this issue Jun 22, 2020
Merged
@jfehrle jfehrle added this to Regular priority in Ltac2 Jun 25, 2020
@ppedrot ppedrot mentioned this issue Mar 13, 2021
Merged
@coqbot-app coqbot-app bot added this to the 8.14+rc1 milestone Mar 23, 2021
@Alizter Alizter moved this from Regular priority to Done in Ltac2 May 17, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
Ltac2
  
Done
Milestone
8.14+rc1
Development

Successfully merging a pull request may close this issue.

Allow to register deprecation status in Ltac2 term and notation declarations ppedrot/coq
1 participant
@JasonGross