From 576d84e4322a9dd7a6d2ffe45172e01182bf44b0 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 11 May 2020 17:41:58 +0200
Subject: Update docgram following #12122 and #12229.

---
 doc/tools/docgram/orderedGrammar | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'doc/tools/docgram/orderedGrammar')

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 11f06b7b8a..3c85b65bca 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -823,7 +823,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT [ "(bfs)" | "(dfs)" ] OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -1085,6 +1085,11 @@ hints_path: [
 | hints_path hints_path
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 class: [
 | "Funclass"
 | "Sortclass"
-- 
cgit v1.2.3