aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorJim Fehrle2020-10-12 21:55:00 -0700
committerJim Fehrle2020-10-27 12:17:21 -0700
commit41b07808c84a86ea4b77e0c7855b22bfd3906669 (patch)
tree0d27eb37c422889247b306630f6440b99ce3618f /lib
parentede77b72328c98995c0636656bb71ba87861ddfe (diff)
Rename misc nonterminals
Diffstat (limited to 'lib')
-rw-r--r--lib/genarg.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 5417a14e6d..aac43db672 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -11,7 +11,7 @@
(** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
(** The route of a generic argument, from parsing to evaluation.
-In the following diagram, "object" can be ltac_expr, constr, tactic_arg, etc.
+In the following diagram, "object" can be ltac_expr, constr, tactic_value, etc.
{% \begin{verbatim} %}
parsing in_raw out_raw