diff options
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index ff1efa5375..0827ccd193 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1435,7 +1435,7 @@ simple_tactic: [ | "notypeclasses" "refine" one_term | "simple" "notypeclasses" "refine" one_term | "solve_constraints" -| "subst" OPT ( LIST1 ident ) +| "subst" LIST0 ident | "simple" "subst" | "evar" "(" ident ":" term ")" | "evar" one_term |