diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 2 | ||||
| -rw-r--r-- | doc/tools/docgram/dune | 6 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 24 |
3 files changed, 19 insertions, 13 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 116fcaa87b..4c1956d172 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2481,7 +2481,6 @@ SPLICE: [ | binders | casted_constr | check_module_types -| constr_pattern | decl_sep | function_fix_definition (* loses funind annotation *) | glob @@ -2655,6 +2654,7 @@ RENAME: [ | ssrfwd ssrdefbody | ssrclauses ssr_in | ssrcpat ssrblockpat +| constr_pattern one_pattern ] simple_tactic: [ diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune index 2a7b283f55..1c07d00d4f 100644 --- a/doc/tools/docgram/dune +++ b/doc/tools/docgram/dune @@ -12,7 +12,6 @@ (glob_files %{project_root}/parsing/*.mlg) (glob_files %{project_root}/toplevel/*.mlg) (glob_files %{project_root}/vernac/*.mlg) - ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) (glob_files %{project_root}/plugins/btauto/*.mlg) (glob_files %{project_root}/plugins/cc/*.mlg) (glob_files %{project_root}/plugins/derive/*.mlg) @@ -23,8 +22,11 @@ (glob_files %{project_root}/plugins/micromega/*.mlg) (glob_files %{project_root}/plugins/nsatz/*.mlg) (glob_files %{project_root}/plugins/omega/*.mlg) - (glob_files %{project_root}/plugins/rtauto/*.mlg) (glob_files %{project_root}/plugins/ring/*.mlg) + (glob_files %{project_root}/plugins/rtauto/*.mlg) + (glob_files %{project_root}/plugins/ssr/*.mlg) + (glob_files %{project_root}/plugins/ssrmatching/*.mlg) + (glob_files %{project_root}/plugins/ssrsearch/*.mlg) (glob_files %{project_root}/plugins/syntax/*.mlg) (glob_files %{project_root}/user-contrib/Ltac2/*.mlg) ; Sphinx files diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 6b12d90d5d..26474d950a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -728,7 +728,11 @@ sort_family: [ ] hint_info: [ -| "|" OPT natural OPT one_term +| "|" OPT natural OPT one_pattern +] + +one_pattern: [ +| one_term ] module_binder: [ @@ -1015,7 +1019,7 @@ command: [ | "Prenex" "Implicits" LIST1 qualid (* SSR plugin *) | "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *) | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *) -| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *) +| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural @@ -1111,9 +1115,9 @@ command: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body ) | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def ) @@ -1171,7 +1175,7 @@ search_query: [ search_item: [ | OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key ) -| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term +| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern | "is" ":" logical_kind ] @@ -1200,7 +1204,7 @@ hint: [ | "Mode" qualid LIST1 [ "+" | "!" | "-" ] | "Unfold" LIST1 qualid | "Constructors" LIST1 qualid -| "Extern" natural OPT one_term "=>" ltac_expr +| "Extern" natural OPT one_pattern "=>" ltac_expr ] tacdef_body: [ @@ -2408,9 +2412,9 @@ tac2mode: [ | "Compute" term | "Check" term | "About" reference OPT univ_name_list -| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) -| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) +| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid ) | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid ) ] |