Commit ad7eeccc authored by Robbert Krebbers's avatar Robbert Krebbers

Mark `iAlways` as deprecated in the code.

It was already marked as deprecated in `doc/proof_mode.md`.
parent 066b7f65
......@@ -1341,6 +1341,8 @@ Tactic Notation "iModIntro" uconstr(sel) :=
|pm_prettify (* reduce redexes created by instantiation *)
(* subgoal *) ].
Tactic Notation "iModIntro" := iModIntro _.
(** DEPRECATED *)
Tactic Notation "iAlways" := iModIntro.
(** * Later *)
......
  • Why not use #[deprecated(note="use iModIntro instead")]?

  • Does that work for tactics? Which minimal Coq versions does it require?

  • Yes, it works for tactics and tactic notations, and attributes (including this attribute) were added in v8.9.

  • Oh, that is cool! But for that to work, we need to drop support for v8.8. I would be in favor of that.

  • Hmm, is there also a proper way of deprecating the !# intro pattern? When I let the intro induction pattern handler iIntros_go translate !# into iAlways, it complains in the definition of iIntros_go...

  • Ralf Jung @jung

    mentioned in merge request !378 (merged)

    ·

    mentioned in merge request !378 (merged)

    Toggle commit list
  • I'm in favor, too: !378 (merged)

Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment