diff options
| author | Théo Zimmermann | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:02:10 +0200 |
| commit | 576d84e4322a9dd7a6d2ffe45172e01182bf44b0 (patch) | |
| tree | 6193c2ce0af15cbe7ed10fd292118c57578c04bc /doc/tools/docgram/orderedGrammar | |
| parent | 03e0aa5ee57b3b539b0fa34be2e1a02a2803b0be (diff) | |
Update docgram following #12122 and #12229.
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 7 |
1 files changed, 6 insertions, 1 deletions
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" |