aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tactic_debug.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-07-14 18:23:31 +0200
committerHugo Herbelin2020-11-22 13:28:40 +0100
commit87c46c50506089ba16bdd7afd7e795ee21033319 (patch)
tree83097b8fb1664f404296e4b4c09ebefe620bd50a /plugins/ltac/tactic_debug.ml
parentdf8b5c7d83ad6e88af34d29bcc32c85bd42c2712 (diff)
Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".
For constr, this means clarifying that "ident" is deprecated and to be replaced by "name". Here, some cleaning shall have to be done at the end of deprecation phase, when "ident" will take its literal meaning. For custom notations, this is about documenting the effect of "ident" and "global" which was yet undocumented. Note that we anticipate an example in constr working with the literal meaning of "ident" (temporarily silencing the warning). Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
0 files changed, 0 insertions, 0 deletions