Merge PR #14594: Update fullgrammar with the removal of new auto

Reviewed-by: Zimmi48 Co-authored-by: Zimmi48 <Zimmi48@users.noreply.github.com>
coq · Jul 3, 2021 · d91d22d · d91d22d
2 parents 4814585 + 584a416
commit d91d22d
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -1640,7 +1640,6 @@ simple_tactic: [
 | "info_auto" OPT nat_or_var auto_using hintbases
 | "debug" "auto" OPT nat_or_var auto_using hintbases
 | "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
-| "new" "auto" OPT nat_or_var auto_using hintbases
 | "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
 | "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
 | "dfs" "eauto" OPT nat_or_var auto_using hintbases

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -1735,7 +1735,6 @@ simple_tactic: [
 | "info_auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "eauto" OPT nat_or_var OPT auto_using OPT hintbases
-| "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases
 | "debug" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases