From cf868740c3d18ee9ce9a6b38dd617784625a3cae Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 9 Jan 2019 15:32:52 -0800 Subject: [PATCH] Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files and inserting it into the .rst files --- .gitattributes | 2 + .gitignore | 3 + Makefile.build | 33 +- Makefile.common | 3 +- coqpp/coqpp_lex.mll | 1 + coqpp/coqpp_main.ml | 28 +- coqpp/coqpp_parse.mly | 60 +- coqpp/coqpp_parser.ml | 44 + coqpp/coqpp_parser.mli | 15 + coqpp/dune | 2 +- doc/tools/docgram/README.md | 208 + doc/tools/docgram/common.edit_mlg | 220 ++ doc/tools/docgram/doc_grammar.ml | 1572 ++++++++ doc/tools/docgram/fullGrammar | 3174 ++++++++++++++++ doc/tools/docgram/orderedGrammar | 4170 +++++++++++++++++++++ doc/tools/docgram/prodn.edit_mlg | 14 + doc/tools/docgram/productionlist.edit_mlg | 25 + 17 files changed, 9543 insertions(+), 31 deletions(-) create mode 100644 coqpp/coqpp_parser.ml create mode 100644 coqpp/coqpp_parser.mli create mode 100644 doc/tools/docgram/README.md create mode 100644 doc/tools/docgram/common.edit_mlg create mode 100644 doc/tools/docgram/doc_grammar.ml create mode 100644 doc/tools/docgram/fullGrammar create mode 100644 doc/tools/docgram/orderedGrammar create mode 100644 doc/tools/docgram/prodn.edit_mlg create mode 100644 doc/tools/docgram/productionlist.edit_mlg diff --git a/.gitattributes b/.gitattributes index 260e3f96b68c..415cabba3b15 100644 --- a/.gitattributes +++ b/.gitattributes @@ -19,6 +19,7 @@ *.dtd whitespace=blank-at-eol,tab-in-indent dune* whitespace=blank-at-eol,tab-in-indent *.dune whitespace=blank-at-eol,tab-in-indent +*.edit_mlg whitespace=blank-at-eol,tab-in-indent *.el whitespace=blank-at-eol,tab-in-indent *.fake whitespace=blank-at-eol,tab-in-indent *.g whitespace=blank-at-eol,tab-in-indent @@ -36,6 +37,7 @@ dune* whitespace=blank-at-eol,tab-in-indent *.mll whitespace=blank-at-eol,tab-in-indent *.mllib whitespace=blank-at-eol,tab-in-indent *.mlp whitespace=blank-at-eol,tab-in-indent +*.mly whitespace=blank-at-eol,tab-in-indent *.mlpack whitespace=blank-at-eol,tab-in-indent *.nix whitespace=blank-at-eol,tab-in-indent *.nsh whitespace=blank-at-eol,tab-in-indent diff --git a/.gitignore b/.gitignore index 5339a0c44d3e..93b874eae3c9 100644 --- a/.gitignore +++ b/.gitignore @@ -110,6 +110,9 @@ doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/html/ doc/stdlib/index-body.html doc/stdlib/index-list.html +doc/tools/docgram/productionlistGrammar +doc/tools/docgram/editedGrammar +doc/tools/docgram/prodnGrammar doc/tutorial/Tutorial.v.out doc/RecTutorial/RecTutorial.html doc/RecTutorial/RecTutorial.ps diff --git a/Makefile.build b/Makefile.build index c6223a6dbd19..d1ed9a6f9638 100644 --- a/Makefile.build +++ b/Makefile.build @@ -355,13 +355,44 @@ kernel/copcodes.ml: kernel/genOpcodeFiles.exe COQPPCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) coqpp/coqpp_parse.cmi: coqpp/coqpp_ast.cmi +coqpp/coqpp_parser.cmo: coqpp_parser.cmi coqpp/coqpp_parse.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo -$(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml +$(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_main.ml $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@ +DOC_GRAMCMO := $(addsuffix .cmo, $(addprefix coqpp/, coqpp_parse coqpp_lex)) + +$(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/tools/docgram/doc_grammar.ml + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) -I coqpp $^ -package str -linkall -linkpkg -o $@ + +DOC_MLGS := */*.mlg plugins/*/*.mlg +DOC_EDIT_MLGS := doc/tools/docgram/*_mlg +DOC_RSTS := doc/sphinx/*.rst doc/sphinx/*/*.rst + +doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) + $(SHOW)'DOC_GRAM' + $(HIDE)$(DOC_GRAM) -short -no-warn $(DOC_MLGS) + +#todo: add a dependency of sphinx on orderedGrammar and of *.rst on orderedGrammar when we're ready +doc/tools/docgram/orderedGrammar: $(DOC_GRAM) $(DOC_EDIT_MLGS) + $(SHOW)'DOC_GRAM_RSTS' + $(HIDE)$(DOC_GRAM) $(DOC_MLGS) $(DOC_RSTS) + +.PHONY: doc_gram doc_gram_rsts doc_gram_verify + +doc_gram: doc/tools/docgram/fullGrammar + +doc_gram_verify: doc/tools/docgram/fullGrammar + $(SHOW)'DOC_GRAM_VERIFY' + $(HIDE)$(DOC_GRAM) -short -no-warn -verify $(DOC_MLGS) $(DOC_RSTS) + +#todo: add dependency on $(DOC_RSTS) very soon +doc_gram_rsts: doc/tools/docgram/orderedGrammar + ########################################################################### # Specific rules for Uint63 ########################################################################### diff --git a/Makefile.common b/Makefile.common index b331484fb217..dd23d7dd2ffa 100644 --- a/Makefile.common +++ b/Makefile.common @@ -22,6 +22,7 @@ COQTOPBYTE:=bin/coqtop.byte$(EXE) COQDEP:=bin/coqdep$(EXE) COQPP:=bin/coqpp$(EXE) +DOC_GRAM:=bin/doc_grammar$(EXE) COQDEPBYTE:=bin/coqdep.byte$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE) @@ -42,7 +43,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) + $(COQWORKMGR) $(COQPP) $(DOC_GRAM) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 040d5eee0943..b1dc841a4cd2 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -100,6 +100,7 @@ rule extend = parse | "COMMAND" { COMMAND } | "TACTIC" { TACTIC } | "EXTEND" { EXTEND } +| "DOC_GRAMMAR" { DOC_GRAMMAR } | "END" { END } | "DECLARE" { DECLARE } | "PLUGIN" { PLUGIN } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 7e869d6fe1b0..72b7cb2f849d 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -11,6 +11,7 @@ open Lexing open Coqpp_ast open Format +open Coqpp_parser let fatal msg = let () = Format.eprintf "Error: %s@\n%!" msg in @@ -19,13 +20,6 @@ let fatal msg = let dummy_loc = { loc_start = Lexing.dummy_pos; loc_end = Lexing.dummy_pos } let mk_code s = { code = s; loc = dummy_loc } -let pr_loc loc = - let file = loc.loc_start.pos_fname in - let line = loc.loc_start.pos_lnum in - let bpos = loc.loc_start.pos_cnum - loc.loc_start.pos_bol in - let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in - Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos - let print_code fmt c = let loc = c.loc.loc_start in (* Print the line location as a source annotation *) @@ -33,26 +27,6 @@ let print_code fmt c = let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in fprintf fmt "@[@<0>%s@]@\n" code_insert -let parse_file f = - let chan = open_in f in - let lexbuf = Lexing.from_channel chan in - let () = lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = f } in - let ans = - try Coqpp_parse.file Coqpp_lex.token lexbuf - with - | Coqpp_lex.Lex_error (loc, msg) -> - let () = close_in chan in - let () = Printf.eprintf "%s\n%!" (pr_loc loc) in - fatal msg - | Parsing.Parse_error -> - let () = close_in chan in - let loc = Coqpp_lex.loc lexbuf in - let () = Printf.eprintf "%s\n%!" (pr_loc loc) in - fatal "syntax error" - in - let () = close_in chan in - ans - module StringSet = Set.Make(String) let string_split s = diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index d1f09c2d0b68..5a0d54c60d9c 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -57,6 +57,8 @@ let parse_user_entry s sep = in parse s sep table +let no_code = { code = ""; loc = { loc_start=Lexing.dummy_pos; loc_end=Lexing.dummy_pos} } + %} %token CODE @@ -64,7 +66,7 @@ let parse_user_entry s sep = %token IDENT QUALID %token STRING %token INT -%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT +%token VERNAC TACTIC GRAMMAR DOC_GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED %token COMMAND CLASSIFIED STATE PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS %token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR @@ -97,6 +99,7 @@ node: | vernac_extend { $1 } | tactic_extend { $1 } | argument_extend { $1 } +| doc_gram { $1 } ; declare_plugin: @@ -411,3 +414,58 @@ gram_tokens: | gram_token { [$1] } | gram_token gram_tokens { $1 :: $2 } ; + +doc_gram: +| DOC_GRAMMAR doc_gram_entries + { GramExt { gramext_name = ""; gramext_globals=[]; gramext_entries = $2 } } + +doc_gram_entries: +| { [] } +| doc_gram_entry doc_gram_entries { $1 :: $2 } +; + +doc_gram_entry: +| qualid_or_ident COLON LBRACKET PIPE doc_gram_rules RBRACKET + { { gentry_name = $1; gentry_pos = None; + gentry_rules = [{ grule_label = None; grule_assoc = None; grule_prods = $5; }] } } +| qualid_or_ident COLON LBRACKET RBRACKET + { { gentry_name = $1; gentry_pos = None; + gentry_rules = [{ grule_label = None; grule_assoc = None; grule_prods = []; }] } } +; + +doc_gram_rules: +| doc_gram_rule { [$1] } +| doc_gram_rule PIPE doc_gram_rules { $1 :: $3 } +; + +doc_gram_rule: +| doc_gram_symbols_opt { { gprod_symbs = $1; gprod_body = no_code; } } +; + +doc_gram_symbols_opt: +| { [] } +| doc_gram_symbols { $1 } +| doc_gram_symbols SEMICOLON { $1 } +; + +doc_gram_symbols: +| doc_gram_symbol { [$1] } +| doc_gram_symbols SEMICOLON doc_gram_symbol { $1 @ [$3] } +; + +doc_gram_symbol: +| IDENT EQUAL doc_gram_gram_tokens { (Some $1, $3) } +| doc_gram_gram_tokens { (None, $1) } +; + +doc_gram_gram_tokens: +| doc_gram_gram_token { [$1] } +| doc_gram_gram_token doc_gram_gram_tokens { $1 :: $2 } +; + +doc_gram_gram_token: +| qualid_or_ident { GSymbQualid ($1, None) } +| LPAREN doc_gram_gram_tokens RPAREN { GSymbParen $2 } +| LBRACKET doc_gram_rules RBRACKET { GSymbProd $2 } +| STRING { GSymbString $1 } +; diff --git a/coqpp/coqpp_parser.ml b/coqpp/coqpp_parser.ml new file mode 100644 index 000000000000..1fa47f554c1e --- /dev/null +++ b/coqpp/coqpp_parser.ml @@ -0,0 +1,44 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* + let () = close_in chan in + let () = Printf.eprintf "%s\n%!" (pr_loc loc) in + fatal msg + | Parsing.Parse_error -> + let () = close_in chan in + let loc = Coqpp_lex.loc lexbuf in + let () = Printf.eprintf "%s\n%!" (pr_loc loc) in + fatal "syntax error" + in + let () = close_in chan in + ans diff --git a/coqpp/coqpp_parser.mli b/coqpp/coqpp_parser.mli new file mode 100644 index 000000000000..6e0a59687a13 --- /dev/null +++ b/coqpp/coqpp_parser.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* string + +val fatal : string -> unit + +val parse_file : string -> Coqpp_ast.t diff --git a/coqpp/dune b/coqpp/dune index a6edf4cf5bba..12071c7c0560 100644 --- a/coqpp/dune +++ b/coqpp/dune @@ -5,5 +5,5 @@ (name coqpp_main) (public_name coqpp) (package coq) - (modules coqpp_ast coqpp_lex coqpp_parse coqpp_main) + (modules coqpp_ast coqpp_lex coqpp_parse coqpp_parser coqpp_main) (modules_without_implementation coqpp_ast)) diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md new file mode 100644 index 000000000000..98fdc38ca7e4 --- /dev/null +++ b/doc/tools/docgram/README.md @@ -0,0 +1,208 @@ +# Grammar extraction tool for documentation + +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in +chunks into `.rst` files. The tool currently inserts Sphinx +`productionlist` constructs. It also generates a file with `prodn` constructs +for the entire grammar, but updates to `tacn` and `cmd` constructs must be done +manually since the grammar doesn't have names for them as it does for +nonterminals. There is an option to report which `tacn` and `cmd` were not +found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. + +The mlg grammars present several challenges to generating an accurate grammar +for documentation purposes: + +* The 30+ mlg files don't define an overall order in which nonterminals should + appear in a complete grammar. + +* Even within a single mlg file, nonterminals and productions are often given + in an order that's much different from what a reader of the documentation would + expect. In a small number of cases, changing the order in the mlg would change + how some inputs are parsed, in particular when the order determines how to distinguish + otherwise ambiguous inputs. + + Strictly speaking, that means our grammar is not a context free grammar even though + we gloss over that distinction in the documentation. + +* For a few nonterminals, some productions are only available if certain plugins + are activated (e.g. SSR). Readers should be informed about these. + +* Some limited parts of the grammar are defined in OCaml, including lookahead symbols + like `test_bracket_ident` and references to nonterminals in other files using + qualified names such as `Prim.ident`. A few symbols are defined multiple times, + such as `scope` and `orient`. + +## What the tool does + +1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes +all the grammar without the actions for each production or the OCaml code. This +file is provided as a convenience to make it easier to examine the (mostly) +unprocessed grammar of the mlg files with less clutter. Nonterminals that use +levels (`"5" RIGHTA` below) are modified, for example: + +``` +tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] +``` + +becomes + +``` +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] +``` + +2. The tool applies grammar editing operations specified by `common.edit_mlg` to +generate `editedGrammar`. + +3. `orderedGrammar` gives the desired order for the nonterminals and productions +in the documented grammar. Developers should edit this file to change the order. +`doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions +as `editedGrammar`. The update process removes manually-added comments from +`orderedGrammar` while automatically-generated comments will be regenerated. + +4. The tool applies further edits to the grammar specified by `productionlist.edit_mlg`, +then it updates the productionlists in the `.rst` files as specified by comments in the form +`.. insertgram `. The edits are primarily to expand +`.mlg` constructs such as `LIST1` and `OPT` into separate productions. The tool +generates `productionlistGrammar`, which has the entire grammar in the form of `productionlists`. + +5. Using the grammar produced in step 3, the tool applies edits specified by +`prodn.edit_mlg` and generates `prodnGrammar`, representing each production as +a Sphinx `prodn` construct. Differently-edited grammars are used because `prodn` +can naturally represent `LIST1 x SEP ','` whereas that is awkward for `productionlists`. + +## How to use the tool + +* `make doc_gram` updates `fullGrammar`. + +* `make doc_gram_verify` verifies that `fullGrammar` is consistent with the `.mlg` files. + This is for use by CI. + +* `make doc_gram_rsts` updates the `*Grammar` and `.rst` files. + +Changes to `fullGrammar`, `orderedGrammar` and the `.rsts` should be checked in to git. +The other `*Grammar` files should not. + +### Command line arguments + +The executable takes a list of `.mlg` and `.rst` files as arguments. The tool +inserts the grammar into the `.rsts` as specified by comments in those files. +The order of the `.mlg` files affects the order of nonterminals and productions in +`fullGrammar`. The order doesn't matter for the `.rst` files. + +Specifying the `-verify` command line argument avoids updating any of the files, +but verifies that the current files are consistent. This setting is meant for +use in CI; it will be up to each developer to include the changes to `*Grammar` and +the `.rst` files in their PRs when they've changed the grammar. + +Other command line arguments: + +* `-check-tacs` reports on differences in tactics between the `rsts` and the grammar + +* `-check-cmds` reports on differences in commands between the `rsts` and the grammar + +* `-no-warn` suppresses printing of some warning messages + +* `-short` limits processing to updating/verifying only the `fullGrammar` file + +* `-verbose` prints more messages about the grammar + +* `-verify` described above + +### Grammar editing scripts + +The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped +of all OCaml features. This is an easy way to include productions to match or add without +writing another parser. The `DOC_GRAMMAR` token at the beginning of each file +signals the use of streamlined syntax. + +Each edit file has a series of items in the form of productions. Items are applied +in the order they appear. There are two types of editing operations: + +* Global edits - edit rules that apply to the entire grammar in a single operation. + These are identified by using specific reserved names as the non-terminal name. + +* Local edits - edit rules that apply to the productions of a single non-terminal. + The rule is a local edit if the non-terminal name isn't reserved. Individual + productions within a local edit that begin with a different set of reserved names + edit existing productions. For example `binders: [ | DELETE Pcoq.Constr.binders ]` + deletes the production `binders: [ | Pcoq.Constr.binders]` + +Productions that don't begin with a reserved name are added to the grammar, +such as `empty: [ | ]`, which adds a new non-terminal `empty` with an +empty production on the right-hand side. + +Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as +the name of a non-terminal and adds one production for it. (We know that LEFTQMARK +is a token but doc_grammar does not.) `SPLICE: [ | LEFTQMARK ]` requests replacing all +uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the +non-terminal. The combined effect of these two is to replace all uses of +`LEFTQMARK` with `"?"`. + +Here are the current operations. They are likely to be refined as we learn +what operations are most useful while we update the mlg files and documentation: + +### Global edits + +`DELETE` - deletes the specified non-terminals anywhere in the grammar. Each +should appear as a separate production. Useful for removing non-terminals that +only do lookahead that shouldn't be in the documentation. + +`RENAME` - each production specifies an (old name, new name) pair of +non-terminals to rename. + +`SPLICE` - requests replacing all uses of the nonterminals anywhere in the +grammar with its productions and removing the non-terminal. Each should appear +as a separate production. (Doesn't work recursively; splicing for both +`A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.) + +`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into +new non-terminals + +### Local edits + +`DELETE ` - removes the specified production from the grammar + +`EDIT ` - modifies the specified production using the following tags +that appear in the specified production: + +* `USE_NT ` LIST* - extracts LIST* as new nonterminal with the specified + new non-terminal name + +* `ADD_OPT ` - looks for a production that matches the specified + production **without** ``. If found, both productions are + replaced with single production with `OPT ` + + The current version handles a single USE_NT or ADD_OPT per EDIT. + +* `REPLACE` - (2 sequential productions) - removes `` and + inserts `` in its place. + +``` +| REPLACE +| WITH +``` + +* (any other nonterminal name) - adds a new production (and possibly a new nonterminal) +to the grammar. + +### `.rst` file updates + +`doc_grammar` updates `.rst` files when it sees the following 3 lines + +``` +.. insertgram +.. productionlist:: XXX +``` + +The end of the existing `productionlist` is recognized by a blank line. + +### Other details + +The output identifies productions from plugins that aren't automatically loaded with +`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists. +If desired, this mechanism could be extended to tag certain productions as deprecated, +perhaps in conjunction with a coqpp change. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg new file mode 100644 index 000000000000..ea94e21ff333 --- /dev/null +++ b/doc/tools/docgram/common.edit_mlg @@ -0,0 +1,220 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* empty *) +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" (* todo: should "_" be a keyword or an identifier? *) +] + +int: [ (* todo: probably should be NUMERAL *) +| integer +] + +command_entry: [ +| noedit_mode +] + +binders: [ +| DELETE Pcoq.Constr.binders (* todo: not sure why there are 2 "binders:" *) +] + +(* edits to simplify *) + +ltac_expr1: [ +| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" +] + +match_context_list: [ +| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|" +] + +match_hyps: [ +| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern +| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern +| DELETE name ":=" match_pattern +] + +match_list: [ +| EDIT ADD_OPT "|" LIST1 match_rule SEP "|" +] + + +selector_body: [ +| REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) +| WITH LIST1 range_selector SEP "," +] + +range_selector_or_nth: [ +| DELETENT +] + +simple_tactic: [ +| DELETE "intros" +| REPLACE "intros" ne_intropatterns +| WITH "intros" intropattern_list_opt +| DELETE "eintros" +| REPLACE "eintros" ne_intropatterns +| WITH "eintros" intropattern_list_opt +] + +intropattern_list_opt: [ +| DELETE LIST0 intropattern +| intropattern_list_opt intropattern +| empty +] + + +ne_intropatterns: [ +| DELETENT (* todo: don't use DELETENT for this *) +] + + +or_and_intropattern: [ +| DELETE "()" +| DELETE "(" simple_intropattern ")" +| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| WITH "(" LIST0 simple_intropattern SEP "," ")" +| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]" +] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml new file mode 100644 index 000000000000..9f0a1942f9d5 --- /dev/null +++ b/doc/tools/docgram/doc_grammar.ml @@ -0,0 +1,1572 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* elt <> nt) !g.order } + + (* rename an nt and update its prods, keeping its original position. + If the new name already exists, include its prods *) + let g_rename_merge g nt nt' nprods = + let oprods = + try + let oprods = NTMap.find nt' !g.map in + g := { !g with order = List.filter (fun elt -> elt <> nt') !g.order }; + oprods + with Not_found -> + g := { !g with map = NTMap.add nt' [] !g.map }; + [] + in + g := { map = NTMap.remove nt !g.map; + order = List.map (fun n -> if n = nt then nt' else n) !g.order }; + g_update_prods g nt' (oprods @ nprods) + + (* add a new nonterminal after "ins_after" None means insert at the beginning *) + let g_add_after g ins_after nt prods = + if NTMap.mem nt !g.map then raise Duplicate; (* don't update the nt if it's already present *) + let rec insert_nt order res = + match ins_after, order with + | None, _ -> nt :: order + | Some _, [] -> raise Not_found + | Some ins_after_nt, hd :: tl -> + if hd = ins_after_nt then + (List.rev res) @ (hd :: nt :: tl) + else + insert_nt tl (hd :: res) + in + g := { order = insert_nt !g.order []; + map = NTMap.add nt prods !g.map } + + (* replace the map and order *) + let g_reorder g map order = + let order_nts = StringSet.of_list order in + let map_nts = List.fold_left (fun res b -> let (nt, _) = b in StringSet.add nt res) + StringSet.empty (NTMap.bindings map) in + if List.length order <> NTMap.cardinal map || + not (StringSet.equal order_nts map_nts) then raise Invalid; + g := { order = order; map = map } + +end +open DocGram + +(*** Print routines ***) + +let sprintf = Printf.sprintf + +let map_and_concat f ?(delim="") l = + String.concat delim (List.map f l) + +let rec db_output_prodn = function + | Sterm s -> sprintf "(Sterm %s) " s + | Snterm s -> sprintf "(Snterm %s) " s + | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) + | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) + | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) + | Sedit s -> sprintf "(Sedit %s) " s + | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 +and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) +and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) + +let rec output_prod plist need_semi = function + | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s + | Snterm s -> + if plist then sprintf "`%s`" s else + sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") + | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) + | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) + | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) + | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) + | Sprod sym_list -> + sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_str r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + | Sedit s -> sprintf "%s" s + (* todo: make PLUGIN info output conditional on the set of prods? *) + | Sedit2 ("PLUGIN", plugin) -> + if plist then + sprintf " (%s plugin)" plugin + else + sprintf " (* %s plugin *)" plugin + | Sedit2 ("FILE", file) -> + let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in + let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in + if plist then + sprintf " (%s)" suffix + else + sprintf " (* %s *)" suffix + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and prod_to_str_r plist prod = + match prod with + | p :: tl -> + let need_semi = + match prod with + | Snterm "IDENT" :: Sterm _ :: _ + | Snterm "IDENT" :: Sprod _ :: _ -> true + | _ -> false in + (output_prod plist need_semi p) :: (prod_to_str_r plist tl) + | [] -> [] + +and prod_to_str ?(plist=false) prod = + String.concat " " (prod_to_str_r plist prod) + + +let rec output_prodn = function + | Sterm s -> let s = if List.mem s ["{"; "{|"; "|"; "}"] then "%" ^ s else s in + sprintf "%s" s + | Snterm s -> sprintf "@%s" s + | Slist1 sym -> sprintf "{+ %s }" (output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "{+%s %s }" (output_sep sep) (output_prodn sym) + | Slist0 sym -> sprintf "{* %s }" (output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "{*%s %s }" (output_sep sep) (output_prodn sym) + | Sopt sym -> sprintf "{? %s }" (output_prodn sym) + | Sparen sym_list -> sprintf "%s" (prod_to_prodn sym_list) + | Sprod sym_list -> + let lcurly, rcurly = if List.length sym_list = 1 then "", "" else "{| ", " }" in + sprintf "%s%s%s" + lcurly + (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_prodn r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + rcurly + | Sedit s -> sprintf "%s" s + | Sedit2 ("PLUGIN", s2) -> "" + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and output_sep sep = + match sep with + | Sterm s -> sprintf "%s" s (* avoid escaping separator *) + | _ -> output_prodn sep + +and prod_to_prodn prod = String.concat " " (List.map output_prodn prod) + +type fmt = [`MLG | `PRODLIST | `PRODN ] + +(* print a subset of the grammar with nts in the specified order *) +let print_in_order out g fmt nt_order hide = + List.iter (fun nt -> + if not (StringSet.mem nt hide) then + try + let prods = NTMap.find nt !g.map in + match fmt with + | `MLG -> + fprintf out "%s: [\n" nt; + List.iter (fun prod -> + let str = prod_to_str ~plist:false prod in + let pfx = if str = "" then "|" else "| " in + fprintf out "%s%s\n" pfx str) + prods; + fprintf out "]\n\n" + | `PRODLIST -> + fprintf out "%s :" nt; + List.iteri (fun i prod -> + if i > 0 then + fprintf out "%s :" (String.make (String.length nt) ' '); + let str = prod_to_str ~plist:true prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + | `PRODN -> + fprintf out "\n%s:\n" nt; + List.iter (fun prod -> + let str = prod_to_prodn prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + with Not_found -> error "Missing nt '%s' in print_in_order\n" nt) + nt_order + + +(*** Read grammar routines ***) + +let cvt_ext prod = + let rec to_doc_sym = function + | Ulist1 sym -> Slist1 (to_doc_sym sym) + | Ulist1sep (sym, s) -> Slist1sep ((to_doc_sym sym), Sterm s) + | Ulist0 sym -> Slist0 (to_doc_sym sym) + | Ulist0sep (sym, s) -> Slist0sep ((to_doc_sym sym), Sterm s) + | Uopt sym -> Sopt (to_doc_sym sym) + | Uentry s -> Snterm s + | Uentryl (s, i) -> Snterm (s ^ (string_of_int i)) + in + let from_ext = function + | ExtTerminal s -> Sterm s + | ExtNonTerminal (s, _) -> to_doc_sym s + in + List.map from_ext prod + +let rec cvt_gram_sym = function + | GSymbString s -> Sterm s + | GSymbQualid (s, level) -> + Snterm (match level with + | Some str -> s ^ str + | None -> s) + | GSymbParen l -> Sparen (cvt_gram_sym_list l) + | GSymbProd ll -> + let cvt = List.map cvt_gram_prod ll in + (match cvt with + | (Snterm x :: []) :: [] -> Snterm x + | (Sterm x :: []) :: [] -> Sterm x + | _ -> Sprod cvt) + +and cvt_gram_sym_list l = + let get_sym = function + | GSymbQualid (s, level) -> s + | _ -> "" + in + + match l with + | GSymbQualid ("LIST0", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist0sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist1sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST0", _) :: s :: tl -> + Slist0 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: tl -> + Slist1 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("OPT", _) :: s :: tl -> + Sopt (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("IDENT", _) :: s2 :: tl when get_sym s2 = "" -> + cvt_gram_sym s2 :: cvt_gram_sym_list tl + | GSymbQualid ("ADD_OPT", _) :: tl -> + (Sedit "ADD_OPT") :: cvt_gram_sym_list tl + | GSymbQualid ("NOTE", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl + | hd :: tl -> + cvt_gram_sym hd :: cvt_gram_sym_list tl + | [] -> [] + +and cvt_gram_prod p = + List.concat (List.map (fun x -> let _, gs = x in cvt_gram_sym_list gs) p.gprod_symbs) + + +let add_symdef nt file symdef_map = + let ent = + try + StringMap.find nt !symdef_map + with Not_found -> [] + in + symdef_map := StringMap.add nt (Filename.basename file::ent) !symdef_map + +let rec edit_SELF nt cur_level next_level right_assoc prod = + let len = List.length prod in + List.mapi (fun i sym -> + match sym with + | Snterm s -> begin match s with + | s when s = nt || s = "SELF" -> + if i = 0 then Snterm next_level + else if i+1 < len then sym + else if right_assoc then Snterm cur_level else Snterm next_level + | "NEXT" -> Snterm next_level + | _ -> sym + end + | Slist1 sym -> Slist1 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | Slist0 sym -> Slist0 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | x -> x) + prod + + +let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) + "parsing/g_constr.mlg"; + "parsing/g_prim.mlg"; + "vernac/g_vernac.mlg"; + "vernac/g_proofs.mlg"; + "toplevel/g_toplevel.mlg"; + "plugins/ltac/extraargs.mlg"; + "plugins/ltac/g_obligations.mlg"; + "plugins/ltac/coretactics.mlg"; + "plugins/ltac/extratactics.mlg"; + "plugins/ltac/profile_ltac_tactics.mlg"; + "plugins/ltac/g_auto.mlg"; + "plugins/ltac/g_class.mlg"; + "plugins/ltac/g_rewrite.mlg"; + "plugins/ltac/g_eqdecide.mlg"; + "plugins/ltac/g_tactic.mlg"; + "plugins/ltac/g_ltac.mlg"; + "plugins/syntax/g_string.mlg"; + "plugins/btauto/g_btauto.mlg"; + "plugins/rtauto/g_rtauto.mlg"; + "plugins/cc/g_congruence.mlg"; + "plugins/firstorder/g_ground.mlg"; + "plugins/syntax/g_numeral.mlg"; +] + + +let ematch prod edit = + let rec ematchr prod edit = + (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) + match (prod, edit) with + | (_, Sedit _ :: tl) + | (_, Sedit2 _ :: tl) + -> ematchr prod tl + | (Sedit _ :: tl, _) + | (Sedit2 _ :: tl, _) + -> ematchr tl edit + | (phd :: ptl, hd :: tl) -> + let m = match (phd, hd) with + | (Slist1 psym, Slist1 sym) + | (Slist0 psym, Slist0 sym) + | (Sopt psym, Sopt sym) + -> ematchr [psym] [sym] + | (Slist1sep (psym, psep), Slist1sep (sym, sep)) + | (Slist0sep (psym, psep), Slist0sep (sym, sep)) + -> ematchr [psym] [sym] && ematchr [psep] [sep] + | (Sparen psyml, Sparen syml) + -> ematchr psyml syml + | (Sprod psymll, Sprod symll) + -> List.fold_left (&&) true (List.map2 ematchr psymll symll) + | _, _ -> phd = hd + in + m && ematchr ptl tl + | ([], hd :: tl) -> false + | (phd :: ptl, []) -> false + | ([], []) -> true +in + (*Printf.printf "\n";*) + let rv = ematchr prod edit in + (*Printf.printf "%b\n" rv;*) + rv + +let has_match p prods = List.exists (fun p2 -> ematch p p2) prods + +let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/" + +let read_mlg is_edit ast file level_renames symdef_map = + let res = ref [] in + let add_prods nt prods = + if not is_edit then + add_symdef nt file symdef_map; + let prods = if not is_edit && + not (List.mem file autoloaded_mlgs) && + Str.string_match plugin_regex file 0 then + let plugin = Str.matched_group 1 file in + List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods + else + prods + in + (* todo: doesn't yet work perfectly with SPLICE *) +(* let prods = if not is_edit then List.map (fun p -> p @ [Sedit2 ("FILE", file)]) prods else prods in*) + res := (nt, prods) :: !res + in + let prod_loop = function + | GramExt grammar_ext -> + let get_label = function + | Some s -> s + | None -> "" + in + List.iter (fun ent -> + let len = List.length ent.gentry_rules in + List.iteri (fun i rule -> + let nt = ent.gentry_name in + let level = (get_label rule.grule_label) in + let level = if level <> "" then level else + match ent.gentry_pos with + | Some Level lev + | Some Before lev + | Some After lev + -> lev + (* Looks like FIRST/LAST can be ignored for documenting the current grammar *) + | _ -> "" in + let cur_level = nt ^ level in + let next_level = nt ^ + if i+1 < len then (get_label (List.nth ent.gentry_rules (i+1)).grule_label) else "" in + let right_assoc = (rule.grule_assoc = Some RightA) in + + if i = 0 && cur_level <> nt && not (StringMap.mem nt !level_renames) then begin + level_renames := StringMap.add nt cur_level !level_renames; + end; + let cvted = List.map cvt_gram_prod rule.grule_prods in + (* edit names for levels *) + (* See https://camlp5.github.io/doc/html/grammars.html#b:Associativity *) + let edited = List.map (edit_SELF nt cur_level next_level right_assoc) cvted in + let prods_to_add = + if cur_level <> nt && i+1 < len then + edited @ [[Snterm next_level]] + else + edited in + add_prods cur_level prods_to_add) + ent.gentry_rules + ) grammar_ext.gramext_entries + + | VernacExt vernac_ext -> + let node = match vernac_ext.vernacext_entry with + | None -> "command" + | Some c -> String.trim c.code + in + add_prods node + (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) + | VernacArgumentExt vernac_argument_ext -> + add_prods vernac_argument_ext.vernacargext_name + (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) + | TacticExt tactic_ext -> + add_prods "simple_tactic" + (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) + | ArgumentExt argument_ext -> + add_prods argument_ext.argext_name + (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) + | _ -> () + in + + List.iter prod_loop ast; + List.rev !res + +let dir s = "doc/tools/docgram/" ^ s + +let read_mlg_edit file = + let fdir = dir file in + let level_renames = ref StringMap.empty in (* ignored *) + let symdef_map = ref StringMap.empty in (* ignored *) + read_mlg true (parse_file fdir) fdir level_renames symdef_map + +let add_rule g nt prods file = + let ent = try NTMap.find nt !g.map with Not_found -> [] in + let nodups = List.concat (List.map (fun prod -> + if has_match prod ent then begin + if !show_warn then + warn "%s: Duplicate production '%s: %s'\n" file nt (prod_to_str prod); + [] + end else + [prod]) + prods) in + g_maybe_add_begin g nt (ent @ nodups) + +let read_mlg_files g args symdef_map = + let level_renames = ref StringMap.empty in + let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in + List.iter (fun file -> + (* does nt renaming, deletion and splicing *) + let rules = read_mlg false (parse_file file) file level_renames symdef_map in + let numprods = List.fold_left (fun num rule -> + let nt, prods = rule in + add_rule g nt prods file; + num + List.length prods) + 0 rules + in + if args.verbose then begin + Printf.eprintf "%s: %d nts, %d prods\n" file (List.length rules) numprods; + if file = last_autoloaded then + Printf.eprintf " Optionally loaded plugins:\n" + end + ) args.mlg_files; + g_reverse g; + !level_renames + + +(*** global editing ops ***) + +let create_edit_map edits = + let rec aux edits map = + match edits with + | [] -> map + | edit :: tl -> + let (key, binding) = edit in + aux tl (StringMap.add key binding map) + in + aux edits StringMap.empty + +(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) +let rec edit_prod g top edit_map prod = + let edit_nt edit_map sym0 nt = + try + let binding = StringMap.find nt edit_map in + match binding with + | "DELETE" -> [] + | "SPLICE" -> + begin + try let splice_prods = NTMap.find nt !g.map in + match splice_prods with + | [] -> assert false + | [p] -> List.rev p + | _ -> [Sprod splice_prods] + with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] + end + | _ -> [Snterm binding] + with Not_found -> [sym0] + in + + let rec edit_symbol sym0 = + match sym0 with + | Sterm s -> [sym0] + | Snterm s -> edit_nt edit_map sym0 s + | Slist1 sym -> [Slist1 (List.hd (edit_symbol sym))] + (* you'll get a run-time failure deleting a SEP symbol *) + | Slist1sep (sym, sep) -> [Slist1sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Slist0 sym -> [Slist0 (List.hd (edit_symbol sym))] + | Slist0sep (sym, sep) -> [Slist0sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Sopt sym -> [Sopt (List.hd (edit_symbol sym))] + | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] + | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in + [Sprod prods] + | Sedit _ + | Sedit2 _ -> [sym0] (* these constructors not used here *) + in + let is_splice nt = + try + StringMap.find nt edit_map = "SPLICE" + with Not_found -> false + in + let get_splice_prods nt = + try NTMap.find nt !g.map + with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) + in + + (* special case splice creating multiple new productions *) + let splice_prods = match prod with + | Snterm nt :: [] when is_splice nt -> + get_splice_prods nt + | _ -> [] + in + if top && splice_prods <> [] then + splice_prods + else + [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] + +and edit_rule g edit_map nt rule = + let nt = + try let new_name = StringMap.find nt edit_map in + match new_name with + | "SPLICE" -> nt + | "DELETE" -> "" + | _ -> new_name + with Not_found -> nt + in + (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) + +(*** splice: replace a reference to a nonterminal with its definition ***) + +(* todo: create a better splice routine, handle recursive case *) +let apply_splice g splice_map = + StringMap.iter (fun nt b -> + if not (NTMap.mem nt !g.map) then + error "Unknown nt '%s' for apply_splice\n" nt) + splice_map; + List.iter (fun b -> + let (nt, prods) = b in + let (nt', prods) = edit_rule g splice_map nt prods in + g_update_prods g nt' prods) + (NTMap.bindings !g.map); + List.iter (fun b -> + let (nt, op) = b in + match op with + | "DELETE" + | "SPLICE" -> + g_remove g nt; + | _ -> ()) + (StringMap.bindings splice_map) + +let find_first edit prods nt = + let rec find_first_r edit prods nt i = + match prods with + | [] -> + error "Can't find '%s' in REPLACE for '%s'\n" (prod_to_str edit) nt; + raise Not_found + | prod :: tl -> + if ematch prod edit then i + else find_first_r edit tl nt (i+1) + in + find_first_r edit prods nt 0 + +let remove_prod edit prods nt = + let res, got_first = List.fold_left (fun args prod -> + let res, got_first = args in + if not got_first && ematch prod edit then + res, true + else + prod :: res, got_first) + ([], false) prods in + if not got_first then + error "Can't find '%s' to DELETE for '%s'\n" (prod_to_str edit) nt; + List.rev res + +let insert_after posn insert prods = + List.concat (List.mapi (fun i prod -> + if i = posn then prod :: insert else [prod]) + prods) + +(*** replace LIST*, OPT with new nonterminals ***) + +(* generate a non-terminal name for a replacement *) +let nt_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_\\.]*$" +let good_name name = if Str.string_match nt_regex name 0 then name else "" +let map_name s = + let s = match s with + | "|" -> "or" + | "!" -> "exclam" + | ">" -> "gt" + | "<" -> "lt" + | "+" -> "plus" + | "?" -> "qmark" + | "}" -> "rbrace" + | "," -> "comma" + | ";" -> "semi" + | _ -> s + in + good_name s + +let rec gen_nt_name sym = + let name_from_prod prod = + let rec aux name sterm_name prod = + if name <> "" then name else + match prod with + | [] -> sterm_name + | Sterm s :: tl + | Snterm s :: tl -> + if good_name s <> "" then + aux (map_name s) sterm_name tl + else + aux name (map_name s) tl; + | sym :: tl-> + aux (gen_nt_name sym) sterm_name tl + in + aux "" "" prod + in + + let name = match sym with + | Sterm s -> map_name s + | Snterm s -> s + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + gen_nt_name sym + | Sparen slist -> + name_from_prod slist + | Sprod slistlist -> + name_from_prod (List.hd slistlist) + | _ -> "" + in + good_name name + +(* create a new nt for LIST* or OPT with the specified name *) +let rec maybe_add_nt g insert_after name sym queue = + let empty = [Snterm "empty"] in + let maybe_unwrap ?(multi=false) sym = + match sym with + | Sprod slist when List.length slist = 1 || multi + -> slist + | Sparen slist -> [ slist ] + | _ -> [ [sym] ] + in + let unw sym = List.hd (maybe_unwrap sym) in + let get_prods nt = + match sym with + | Slist1 sym -> let sym' = unw sym in + [ [Snterm nt] @ sym'; sym' ] + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) -> let sym' = unw sym in + [ [Snterm nt; sep] @ sym'; sym' ] + | Slist0 sym -> [ [Snterm nt] @ (unw sym); empty ] + | Sopt sym -> (maybe_unwrap ~multi:true sym) @ [ empty ] + | Sprod slistlist -> slistlist + | _ -> [] + in + + let is_slist0sep sym = + match sym with + | Slist0sep _ -> true + | _ -> false + in + + (* find an existing nt with an identical definition, or generate an unused nt name *) + let rec find_name nt i = + let trial_name = sprintf "%s%s" nt (if i = 1 then "" else string_of_int i) in + try + if NTMap.find trial_name !g.map = get_prods trial_name then + trial_name + else + find_name nt (succ i) + with Not_found -> trial_name + in + let list_name sep = + match sep with + | Sterm s -> + let name = map_name s in + if name = s then "_list" else "_list_" ^ name + | _ -> "_list" + in + let nt = name ^ match sym with + | Slist1 sym -> "_list" + | Slist1sep (sym, sep) -> list_name sep + | Slist0 sym -> "_list_opt" + | Slist0sep (sym, sep) -> list_name sep (* special handling *) + | Sopt sym -> "_opt" + | Sprod slistlist -> "_alt" + | _ -> (error "Invalid symbol for USE_NT for nt '%s'\n" name; "ERROR") + in + let base_nt = find_name nt 1 in + let new_nt = if is_slist0sep sym then base_nt ^ "_opt" else base_nt in + if not (NTMap.mem new_nt !g.map) then begin + let prods = if is_slist0sep sym then [ [Snterm base_nt]; empty ] else get_prods base_nt in + g_add_after g (Some !insert_after) new_nt prods; + insert_after := new_nt; + Queue.add new_nt queue + end; + if is_slist0sep sym && not (NTMap.mem base_nt !g.map) then begin + match sym with + | Slist0sep (sym, sep) -> + let prods = get_prods base_nt in + g_add_after g (Some !insert_after) base_nt prods; + insert_after := base_nt; + Queue.add base_nt queue + | _ -> () + end; + new_nt + +(* expand LIST*, OPT and add "empty" *) +(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *) +and expand_rule g edited_nt queue = + let rule = NTMap.find edited_nt !g.map in + let insert_after = ref edited_nt in + let rec expand rule = + let rec aux syms res = + match syms with + | [] -> res + | sym0 :: tl -> + let new_sym = match sym0 with + | Sterm _ + | Snterm _ -> + sym0 + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + let name = gen_nt_name sym in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name sym0 queue in + Snterm new_nt + end else sym0 + | Sparen slist -> Sparen (expand slist) + | Sprod slistlist -> + let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in + let name = gen_nt_name sym0 in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name + (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) )) + else sym0) queue + in + Snterm new_nt + end else + Sprod (List.map expand slistlist) + | Sedit _ + | Sedit2 _ -> + sym0 (* these constructors not used here *) + in + aux tl (new_sym :: res) + in + List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else [])) + in + let rule' = List.map expand rule in + g_update_prods g edited_nt rule' + +let expand_lists g = + (* todo: use Queue.of_seq w OCaml 4.07+ *) + let queue = Queue.create () in + List.iter (fun nt -> Queue.add nt queue) !g.order; + try + while true do + let nt = Queue.pop queue in + expand_rule g nt queue + done + with + | Queue.Empty -> () + +let edit_all_prods g op eprods = + let do_it op eprods num = + let rec aux eprods res = + match eprods with + | [] -> res + | [Snterm old_nt; Snterm new_nt] :: tl when num = 2 -> + aux tl ((old_nt, new_nt) :: res) + | [Snterm old_nt] :: tl when num = 1 -> + aux tl ((old_nt, op) :: res) + | eprod :: tl -> + error "Production '%s: %s' must have only %d nonterminal(s)\n" + op (prod_to_str eprod) num; + aux tl res + in + let map = create_edit_map (aux eprods []) in + if op = "SPLICE" then + apply_splice g map + else (* RENAME/DELETE *) + List.iter (fun b -> let (nt, _) = b in + let prods = try NTMap.find nt !g.map with Not_found -> [] in + let (nt', prods') = edit_rule g map nt prods in + if nt' = "" then + g_remove g nt + else if nt <> nt' then + g_rename_merge g nt nt' prods' + else + g_update_prods g nt prods') + (NTMap.bindings !g.map); + in + match op with + | "RENAME" -> do_it op eprods 2; true + | "DELETE" -> do_it op eprods 1; true + | "SPLICE" -> do_it op eprods 1; true + | "EXPAND" -> + if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then + error "'EXPAND:' expects a single empty production\n"; + expand_lists g; true + | _ -> false + +let edit_single_prod g edit0 prods nt = + let rec edit_single_prod_r edit prods nt seen = + match edit with + | [] -> prods + | Sedit "ADD_OPT" :: sym :: tl -> + let prods' = (try + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Sopt sym :: tl)] prods in + let prods = remove_prod (pfx @ (sym :: tl)) prods nt in + remove_prod (pfx @ tl) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit "ADD_OPT" :: [] -> error "Bad position for ADD_OPT\n"; prods + | Sedit2 ("USE_NT", name) :: sym :: tl -> + let prods' = (try + let nt = maybe_add_nt g (ref nt) name sym (Queue.create ()) in + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Snterm nt :: tl)] prods in + remove_prod (pfx @ (sym :: tl)) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit2 ("USE_NT", _) :: [] -> error "Bad position for USE_NT\n"; prods + | sym :: tl -> + edit_single_prod_r tl prods nt (sym :: seen) + in + edit_single_prod_r edit0 prods nt [] + +let apply_edit_file g edits = + List.iter (fun b -> + let (nt, eprod) = b in + if not (edit_all_prods g nt eprod) then begin + let rec aux eprod prods add_nt = + match eprod with + | [] -> prods, add_nt + | (Snterm "DELETE" :: oprod) :: tl -> + aux tl (remove_prod oprod prods nt) add_nt + | (Snterm "DELETENT" :: _) :: tl -> (* note this doesn't remove references *) + g_remove g nt; + aux tl prods false + | (Snterm "EDIT" :: oprod) :: tl -> + aux tl (edit_single_prod g oprod prods nt) add_nt + | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl -> + let prods' = (try + let posn = find_first oprod prods nt in + let prods = insert_after posn [rprod] prods in (* insert new prod *) + remove_prod oprod prods nt (* remove orig prod *) + with Not_found -> prods) + in + aux tl prods' add_nt + | (Snterm "REPLACE" :: _ as eprod) :: tl -> + error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt; + aux tl prods add_nt + | prod :: tl -> + (* add a production *) + if has_match prod prods then + error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt; + aux tl (prods @ [prod]) add_nt + in + let prods, add_nt = + aux eprod (try NTMap.find nt !g.map with Not_found -> []) true in + if add_nt then + g_maybe_add g nt prods + end) + edits + + +(*** main routines ***) + + (* get the nt's in the production, preserving order, don't worry about dups *) + let nts_in_prod prod = + let rec traverse = function + | Sterm s -> [] + | Snterm s -> [s] + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse sym @ (traverse sep) + | Sparen sym_list -> List.concat (List.map traverse sym_list) + | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list) + | Sedit _ + | Sedit2 _ -> [] + in + List.rev (List.concat (List.map traverse prod)) + +(* get the transitive closure of a non-terminal excluding "stops" symbols. + Preserve ordering to the extent possible *) +(* todo: at the moment, the code doesn't use the ordering; consider switching to using +sets instead of lists *) +let nt_closure g start stops = + let stop_set = StringSet.of_list stops in + let rec nt_closure_r res todo = + match todo with + | [] -> res + | nt :: tl -> + if List.mem nt res || StringSet.mem nt stop_set then + nt_closure_r res tl + else begin + let more_to_do = + try + let prods = NTMap.find nt !g.map in + tl @ (List.concat (List.map nts_in_prod prods)) + with Not_found -> tl in + nt_closure_r (nt :: res) more_to_do + end + in + List.rev (nt_closure_r [] [start]) + +let header = "--------------------------------------------" +let nt_subset_in_orig_order g nts = + let subset = StringSet.of_list nts in + List.filter (fun nt -> StringSet.mem nt subset) !g.order + +let print_chunk out g seen fmt title starts ends = + fprintf out "\n\n%s:\n%s\n" title header; + List.iter (fun start -> + let nts = (nt_closure g start ends) in + print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen; + seen := StringSet.union !seen (StringSet.of_list nts)) + starts + +let print_chunks g out fmt () = + let seen = ref StringSet.empty in + print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"]; + print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"]; + print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"]; + print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"]; + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] + ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"]; + + (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*) + print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"]; + print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"]; + print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"]; + print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"]; + print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"]; + print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] []; + + + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] []; + print_chunk out g seen fmt "vernac_control" ["vernac_control"] [] + + (* + let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in + seen := StringSet.union !seen (StringSet.of_list ssr_tops); + + print_chunk out g seen fmt "ssrindex" ["ssrindex"] []; + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "binder_constr" ["binder_constr"] []; + (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*) + print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] []; + (*print_chunk out g seen fmt "hloc" ["hloc"] [];*) + (*print_chunk out g seen fmt "hypident" ["hypident"] [];*) + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] []; + print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] []; + fprintf out "\n\nRemainder:\n"; + print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty; + *) + + + (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) + (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) + +let start_symbols = ["vernac_toplevel"; "tactic_mode"] +let tokens = [ "BULLET"; "FIELD"; "IDENT"; "NUMERAL"; "STRING" ] (* don't report as undefined *) + +let report_bad_nts g file = + let rec get_nts refd defd bindings = + match bindings with + | [] -> refd, defd + | (nt, prods) :: tl -> + get_nts (List.fold_left (fun res prod -> + StringSet.union res (StringSet.of_list (nts_in_prod prod))) + refd prods) + (StringSet.add nt defd) tl + in + let all_nts_ref, all_nts_def = + get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in + + let undef = StringSet.diff all_nts_ref all_nts_def in + List.iter (fun nt -> warn "%s: Undefined symbol '%s'\n" file nt) (StringSet.elements undef); + + let reachable = + List.fold_left (fun res sym -> + StringSet.union res (StringSet.of_list (nt_closure g sym []))) + StringSet.empty start_symbols + in + let unreachable = List.filter (fun nt -> not (StringSet.mem nt reachable)) !g.order in + List.iter (fun nt -> warn "%s: Unreachable symbol '%s'\n" file nt) unreachable + + +let report_info g symdef_map = + let num_prods = List.fold_left (fun sum nt -> let prods = NTMap.find nt !g.map in sum + (List.length prods)) + 0 !g.order + in + + Printf.eprintf "\nstart symbols: %s\n" (String.concat " " start_symbols); + Printf.eprintf "%d nonterminals defined, %d productions\n" (NTMap.cardinal !g.map) num_prods; + Printf.eprintf "%d terminals\n" (List.length tokens); + + Printf.eprintf "\nSymbols with multiple definition points in *.mlg:\n"; + let bindings = List.sort (fun a b -> let (ak, _) = a and (bk, _) = b in + String.compare ak bk) (StringMap.bindings symdef_map) in + List.iter (fun b -> + let (k, v) = b in + if List.length v > 1 then begin + Printf.eprintf " %s: " k; + List.iter (fun f -> Printf.eprintf "%s " f) v; + Printf.eprintf "\n" + end) + bindings; + Printf.eprintf "\n" + + + +[@@@ocaml.warning "-32"] +let rec dump prod = + match prod with + | hd :: tl -> let s = (match hd with + | Sterm s -> sprintf "Sterm %s" s + | Snterm s -> sprintf "Snterm \"%s\"" s + | Slist1 sym -> "Slist1" + | Slist0 sym -> "Slist0" + | Sopt sym -> "Sopt" + | Slist1sep _ -> "Slist1sep" + | Slist0sep _ -> "Slist0sep" + | Sparen sym_list -> "Sparen" + | Sprod sym_list_list -> "Sprod" + | Sedit _ -> "Sedit" + | Sedit2 _ -> "Sedit2") in + Printf.printf "%s " s; + dump tl + | [] -> Printf.printf "\n" +[@@@ocaml.warning "+32"] + +let reorder_grammar eg reordered_rules file = + let og = ref { map = NTMap.empty; order = [] } in + List.iter (fun rule -> + let nt, prods = rule in + try + (* only keep nts and prods in common with editedGrammar *) + let eg_prods = NTMap.find nt !eg.map in + let prods = List.filter (fun prod -> (has_match prod eg_prods)) prods in + if NTMap.mem nt !og.map then + warn "%s: Duplicate nonterminal '%s'\n" file nt; + add_rule og nt prods file + with Not_found -> ()) + reordered_rules; + g_reverse og; + + (* insert a prod in a list after prev_prod (None=at the beginning) *) + let rec insert_prod prev_prod prod prods res = + match prev_prod, prods with + | None, _ -> prod :: prods + | Some _, [] -> raise Not_found + | Some ins_after_prod, hd :: tl -> + if ematch hd ins_after_prod then + (List.rev res) @ (hd :: prod :: tl) + else + insert_prod prev_prod prod tl (hd :: res) + in + + (* insert prods that are not already in og_prods *) + let rec upd_prods prev_prod eg_prods og_prods = + match eg_prods with + | [] -> og_prods + | prod :: tl -> + let og_prods = + if has_match prod og_prods then + List.map (fun p -> if ematch p prod then prod else p) og_prods + else + insert_prod prev_prod prod og_prods [] in + upd_prods (Some prod) tl og_prods + in + + (* add nts and prods not present in orderedGrammar *) + let _ = List.fold_left (fun prev_nt nt -> + let e_prods = NTMap.find nt !eg.map in + if not (NTMap.mem nt !og.map) then + g_add_after og prev_nt nt e_prods + else + g_update_prods og nt (upd_prods None e_prods (NTMap.find nt !og.map)); + Some nt) + None !eg.order in + g_reorder eg !og.map !og.order + + +let finish_with_file old_file verify = + let files_eq f1 f2 = + let chunksize = 8192 in + (try + let ofile = open_in_bin f1 in + let nfile = open_in_bin f2 in + let rv = if (in_channel_length ofile) <> (in_channel_length nfile) then false + else begin + let obuf = Bytes.create chunksize in + Bytes.fill obuf 0 chunksize '\x00'; + let nbuf = Bytes.create chunksize in + Bytes.fill nbuf 0 chunksize '\x00'; + let rec read () = + let olen = input ofile obuf 0 chunksize in + let _ = input nfile nbuf 0 chunksize in + if obuf <> nbuf then + false + else if olen = 0 then + true + else + read () + in + read () + end + in + close_in ofile; + close_in nfile; + rv + with Sys_error _ -> false) + in + + let temp_file = (old_file ^ "_temp") in + if verify then + if (files_eq old_file temp_file || !exit_code <> 0) then + Sys.remove temp_file + else + error "%s is not current\n" old_file + else + Sys.rename temp_file old_file + +let open_temp_bin file = + open_out_bin (sprintf "%s_temp" file) + +let find_longest_match prods str = + (* todo: require a minimum length? *) + let common_prefix_len s1 s2 = + let limit = min (String.length s1) (String.length s2) in + let rec aux off = + if off = limit then off + else if s1.[off] = s2.[off] then aux (succ off) + else off + in + aux 0 + in + + let slen = String.length str in + let rec longest best multi best_len prods = + match prods with + | [] -> best, multi, best_len + | prod :: tl -> + let pstr = String.trim (prod_to_prodn prod) in + let clen = common_prefix_len str pstr in + if clen = slen && slen = String.length pstr then + pstr, false, clen (* exact match *) + else if clen > best_len then + longest pstr false clen tl (* better match *) + else if clen = best_len then + longest best true best_len tl (* 2nd match with same length *) + else + longest best multi best_len tl (* worse match *) + in + longest "" false 0 prods + +type seen = { + nts: (string * int) NTMap.t; + tacs: (string * int) NTMap.t; + cmds: (string * int) NTMap.t; +} + +let process_rst g file args seen tac_prods cmd_prods = + let old_rst = open_in file in + let new_rst = open_temp_bin file in + let linenum = ref 0 in + let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]*\\)\\(.*\\)" in + let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in + let blank_regex = Str.regexp "^[ \t]*$" in + let end_prodlist_regex = Str.regexp "^[ \t]*$" in + let rec index_of_r str list index = + match list with + | [] -> None + | hd :: list -> + if hd = str then Some index + else index_of_r str list (index+1) + in + let index_of str list = index_of_r str list 0 in + let getline () = + let line = input_line old_rst in + incr linenum; + line + in + let output_insertgram start_index end_ indent is_coq_group = + let rec nthcdr n list = if n = 0 then list else nthcdr (n-1) (List.tl list) in + let rec copy_prods list = + match list with + | [] -> () + | nt :: tl -> + (try + let (prev_file, prev_linenum) = NTMap.find nt !seen.nts in + warn "%s line %d: '%s' already included at %s line %d\n" + file !linenum nt prev_file prev_linenum; + with Not_found -> + if is_coq_group then + seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} ); + let prods = NTMap.find nt !g.map in + List.iteri (fun i prod -> + let rhs = String.trim (sprintf ": %s" (prod_to_str ~plist:true prod)) in + fprintf new_rst "%s %s %s\n" indent (if i = 0 then nt else String.make (String.length nt) ' ') rhs) + prods; + if nt <> end_ then copy_prods tl + in + copy_prods (nthcdr start_index !g.order) + in + + let process_insertgram line rhs = + if not (Str.string_match ig_args_regex rhs 0) then + error "%s line %d: bad arguments '%s' for 'insertgram'\n" file !linenum rhs + else begin + let start = Str.matched_group 1 rhs in + let end_ = Str.matched_group 2 rhs in + let start_index = index_of start !g.order in + let end_index = index_of end_ !g.order in + if start_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum start; + if end_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum end_; + match start_index, end_index with + | Some start_index, Some end_index -> + if start_index > end_index then + error "%s line %d: '%s' must appear before '%s' in .../orderedGrammar\n" file !linenum start end_ + else begin + try + let line2 = getline() in + if not (Str.string_match blank_regex line2 0) then + error "%s line %d: expecting a blank line after 'insertgram'\n" file !linenum + else begin + let line3 = getline() in + if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "productionlist::" then + error "%s line %d: expecting 'productionlist' after 'insertgram'\n" file !linenum + else begin + let indent = Str.matched_group 1 line3 in + let is_coq_group = ("coq" = String.trim (Str.matched_group 3 line3)) in + let rec skip_to_end () = + let endline = getline() in + if Str.string_match end_prodlist_regex endline 0 then begin + fprintf new_rst "%s\n\n%s\n" line line3; + output_insertgram start_index end_ indent is_coq_group; + fprintf new_rst "%s\n" endline + end else + skip_to_end () + in + skip_to_end () + end + end + with End_of_file -> error "%s line %d: unexpected end of file\n" file !linenum; + end + | _ -> () + end + + in + try + while true do + let line = getline() in + if Str.string_match dir_regex line 0 then begin + let dir = Str.matched_group 2 line in + let rhs = String.trim (Str.matched_group 3 line) in + match dir with + | "productionlist::" -> + if rhs = "coq" then + warn "%s line %d: Missing 'insertgram' before 'productionlist:: coq'\n" file !linenum; + fprintf new_rst "%s\n" line; + | "tacn::" when args.check_tacs -> + if not (StringSet.mem rhs tac_prods) then + warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.tacs then + warn "%s line %d: Repeated tactic: '%s'\n" file !linenum rhs; + seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)}; + fprintf new_rst "%s\n" line + | "cmd::" when args.check_cmds -> + if not (StringSet.mem rhs cmd_prods) then + warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.cmds then + warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs; + seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)}; + fprintf new_rst "%s\n" line + | "insertgram" -> + process_insertgram line rhs + | _ -> fprintf new_rst "%s\n" line + end else + fprintf new_rst "%s\n" line; + done + with End_of_file -> (); + close_in old_rst; + close_out new_rst; + finish_with_file file args.verify + +let report_omitted_prods entries seen label split = + let maybe_warn first last n = + if first <> "" then begin + if first <> last then + warn "%ss '%s' to %s'%s' not included in .rst files (%d)\n" label first split last n + else + warn "%s %s not included in .rst files\n" label first; + end + in + + let first, last, n = List.fold_left (fun missing nt -> + let first, last, n = missing in + if NTMap.mem nt seen then begin + maybe_warn first last n; + "", "", 0 + end else + (if first = "" then nt else first), nt, n + 1) + ("", "", 0) entries in + maybe_warn first last n + +let process_grammar args = + let symdef_map = ref StringMap.empty in + let g = ref { map = NTMap.empty; order = [] } in + + let level_renames = read_mlg_files g args symdef_map in + + (* rename nts with levels *) + List.iter (fun b -> let (nt, prod) = b in + let (_, prod) = edit_rule g level_renames nt prod in + g_update_prods g nt prod) + (NTMap.bindings !g.map); + + (* print the full grammar with minimal editing *) + let out = open_temp_bin (dir "fullGrammar") in + fprintf out "%s\n%s\n\n" + "(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "fullGrammar") args.verify; + + if not args.fullGrammar then begin + (* do shared edits *) + if !exit_code = 0 then begin + let common_edits = read_mlg_edit "common.edit_mlg" in + apply_edit_file g common_edits + end; + let prodn_gram = ref { map = !g.map; order = !g.order } in + + if !exit_code = 0 && not args.verify then begin + let prodlist_edits = read_mlg_edit "productionlist.edit_mlg" in + apply_edit_file g prodlist_edits; + let out = open_temp_bin (dir "productionlistGrammar") in + if args.verbose then + report_info g !symdef_map; + print_in_order out g `PRODLIST !g.order StringSet.empty; + (*print_chunks g out `PRODLIST ();*) + close_out out; + finish_with_file (dir "productionlistGrammar") args.verify; + end; + + if !exit_code = 0 && not args.verify then begin + let out = open_temp_bin (dir "editedGrammar") in + fprintf out "%s\n%s\n\n" + "(* Edited Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "editedGrammar") args.verify; + report_bad_nts g "editedGrammar" + end; + + if !exit_code = 0 then begin + let ordered_grammar = read_mlg_edit "orderedGrammar" in + let out = open_temp_bin (dir "orderedGrammar") in + fprintf out "%s\n%s\n\n" + ("(* Defines the order to apply to editedGrammar to get productionlistGrammar.\n" ^ + "doc_grammar will modify this file to add/remove nonterminals and productions\n" ^ + "to match editedGrammar, which will remove comments. Not compiled into Coq *)") + "DOC_GRAMMAR"; + reorder_grammar g ordered_grammar "orderedGrammar"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "orderedGrammar") args.verify; + end; + + if !exit_code = 0 then begin + let plist nt = + let list = (List.map (fun t -> String.trim (prod_to_prodn t)) + (NTMap.find nt !g.map)) in + list, StringSet.of_list list in + let tac_list, tac_prods = plist "simple_tactic" in + let cmd_list, cmd_prods = plist "command" in + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in + List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; + report_omitted_prods !g.order !seen.nts "Nonterminal" ""; + if args.check_tacs then + report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; + if args.check_cmds then + report_omitted_prods cmd_list !seen.cmds "Command" "\n " + end; + + (* generate output for prodn: simple_tactic, command, also for Ltac?? *) + if !exit_code = 0 && not args.verify then begin + let prodn_edits = read_mlg_edit "prodn.edit_mlg" in + apply_edit_file prodn_gram prodn_edits; + let out = open_temp_bin (dir "prodnGrammar") in + print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; + close_out out; + finish_with_file (dir "prodnGrammar") args.verify + end + end + +let parse_args () = + let suffix_regex = Str.regexp ".*\\.\\([a-z]+\\)$" in + let args = + List.fold_left (fun args arg -> + match arg with + | "-check-cmds" -> { args with check_cmds = true } + | "-check-tacs" -> { args with check_tacs = true } + | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-short" -> { args with fullGrammar = true } + | "-verbose" -> { args with verbose = true } + | "-verify" -> { args with verify = true } + | arg when Str.string_match suffix_regex arg 0 -> + (match Str.matched_group 1 arg with + | "mlg" -> { args with mlg_files = (arg :: args.mlg_files) } + | "rst" -> { args with rst_files = (arg :: args.rst_files) } + | _ -> error "Unknown command line argument '%s'\n" arg; args) + | arg -> error "Unknown command line argument '%s'\n" arg; args) + default_args (List.tl (Array.to_list Sys.argv)) in + { args with mlg_files = (List.rev args.mlg_files); rst_files = (List.rev args.rst_files)} + +let () = + (*try*) + Printexc.record_backtrace true; + let args = parse_args () in + if !exit_code = 0 then begin + process_grammar args + end; + exit !exit_code + (*with _ -> Printexc.print_backtrace stdout; exit 1*) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar new file mode 100644 index 000000000000..a83638dd73c1 --- /dev/null +++ b/doc/tools/docgram/fullGrammar @@ -0,0 +1,3174 @@ +(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) +DOC_GRAMMAR + +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +lconstr_pattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| operconstr200 +| l_constr +] + +constr: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 LIST1 appl_arg +| "@" global instance LIST0 operconstr9 +| "@" pattern_identref LIST1 identref +| operconstr9 +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global LIST0 appl_arg ")" +| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" Pltac.tactic_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +instance: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" LIST1 fix_decl SEP "with" "for" identref +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMERAL +| string +] + +impl_ident_tail: [ +| "}" +| LIST1 name ":" lconstr "}" +| LIST1 name "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +| "{" "struct" name "}" +| +] + +impl_name_head: [ +| impl_ident_head +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "'" pattern0 +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" [ "!" | ] operconstr200 +| name_colon [ "!" | ] operconstr200 +| operconstr200 +] + +type_cstr: [ +| OPT [ ":" lconstr ] +| ":" lconstr +| +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +pattern_identref: [ +| pattern_ident +] + +var: [ +| ident +] + +identref: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +| _natural +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| Pvernac.Vernac_.main_entry +] + +opt_hintbases: [ +| +| ":" LIST1 IDENT +] + +command: [ +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" identref +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" identref +| "Defined" +| "Defined" identref +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT; [ "discriminated" | ] +| "Remove" "Hints" LIST1 global opt_hintbases +| "Hint" hint opt_hintbases +| "Comments" LIST0 comment +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" [ "Verbose" | ] [ ne_string | IDENT ] +| "Declare" "ML" "Module" LIST1 ne_string +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global OPT univ_name_list +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT LIST1 option_ref_value +| "Add" IDENT LIST1 option_ref_value +| "Test" option_table "for" LIST1 option_ref_value +| "Test" option_table +| "Remove" IDENT IDENT LIST1 option_ref_value +| "Remove" IDENT LIST1 option_ref_value +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" identref +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Derive" ident "SuchThat" constr "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" string LIST1 global (* extraction plugin *) +| "Extraction" "TestCompile" LIST1 global (* extraction plugin *) +| "Separate" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" LIST1 global (* extraction plugin *) +| "Extraction" "NoInline" LIST1 global (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" LIST0 int_or_id "]" (* extraction plugin *) +| "Extraction" "Blacklist" LIST1 ident (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global LIST0 string "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr +| "Hint" "Rewrite" orient LIST1 constr "using" tactic +| "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" constr +| "Derive" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Inversion" ident "with" constr +| "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Declare" "Left" "Step" constr +| "Declare" "Right" "Step" constr +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" constr constr +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" LIST0 reference +| "Typeclasses" "Opaque" LIST0 reference +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int +| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] +| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" LIST1 ltac_tacdef_body SEP "with" +| "Print" "Ltac" "Signatures" +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Setoid" constr constr constr "as" ident +| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident +| "Add" "Morphism" constr ":" ident +| "Declare" "Morphism" constr ":" ident +| "Add" "Morphism" constr "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Add" "Ring" ident ":" constr OPT ring_mods (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" LIST1 global (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* ssr plugin *) +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "String" "Notation" reference reference reference ":" ident +] + +reference_or_constr: [ +| global +| constr +] + +hint: [ +| "Resolve" LIST1 reference_or_constr hint_info +| "Resolve" "->" LIST1 global OPT natural +| "Resolve" "<-" LIST1 global OPT natural +| "Immediate" LIST1 reference_or_constr +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" LIST1 global +| "Opaque" LIST1 global +| "Mode" global mode +| "Unfold" LIST1 global +| "Constructors" LIST1 global +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| LIST1 [ "+" | "!" | "-" ] +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| LIST0 quoted_attributes vernac +] + +quoted_attributes: [ +| "#[" attribute_list "]" +] + +attribute_list: [ +| LIST0 attribute SEP "," +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list ")" +| +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" identref def_body +| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| "Fixpoint" LIST1 rec_definition SEP "with" +| "Let" "Fixpoint" LIST1 rec_definition SEP "with" +| "CoFixpoint" LIST1 corec_definition SEP "with" +| "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| "Scheme" LIST1 scheme SEP "with" +| "Combined" "Scheme" identref "from" LIST1 identref SEP "," +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| "Universe" LIST1 identref +| "Universes" LIST1 identref +| "Constraint" LIST1 univ_constraint SEP "," +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| +] + +univ_constraint: [ +| universe_name [ "<" | "=" | "<=" ] universe_name +] + +univ_decl: [ +| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +] + +ident_decl: [ +| identref OPT univ_decl +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| +] + +one_decl_notation: [ +| ne_lstring ":=" constr OPT [ ":" IDENT ] +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" LIST1 one_decl_notation SEP decl_sep +| +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| +] + +inductive_definition: [ +| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" LIST1 constructor SEP "|" +| identref constructor_type "|" LIST0 constructor SEP "|" +| identref constructor_type +| identref "{" record_fields "}" +| "{" record_fields "}" +| +] + +opt_coercion: [ +| ">" +| +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +] + +scheme: [ +| scheme_kind +| identref ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| LIST1 assum_coe +| simple_assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| LIST1 ident_decl of_type_with_opt_coercion lconstr +] + +constructor_type: [ +| binders [ of_type_with_opt_coercion lconstr | ] +] + +constructor: [ +| identref constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token identref LIST0 module_binder of_module_type is_module_expr +| "Module" "Type" identref LIST0 module_binder check_module_types is_module_type +| "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl +| "Section" identref +| "Chapter" identref +| "End" identref +| "Collection" identref ":=" section_subset_expr +| "Require" export_token LIST1 global +| "From" global "Require" export_token LIST1 global +| "Import" LIST1 global +| "Export" LIST1 global +| "Include" module_type_inl LIST0 ext_module_expr +| "Include" "Type" module_type_inl LIST0 ext_module_type +| "Transparent" LIST1 smart_global +| "Opaque" LIST1 smart_global +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] +| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ] +| "Canonical" OPT "Structure" by_notation +| "Coercion" global OPT univ_decl def_body +| "Identity" "Coercion" identref ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" LIST1 binder +| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Existing" "Instance" global hint_info +| "Existing" "Instances" LIST1 global OPT [ "|" natural ] +| "Existing" "Class" global +| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +export_token: [ +| "Import" +| "Export" +| +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| LIST0 check_module_type +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl LIST0 ext_module_type +| +] + +is_module_expr: [ +| ":=" module_expr_inl LIST0 ext_module_expr +| +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token LIST1 identref ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| only_starredidentrefs LIST0 starredidentref +| ssexpr35 +] + +starredidentref: [ +| identref +| identref "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" only_starredidentrefs LIST0 starredidentref ")" +| "(" only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| OPT "!" name OPT scope +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" LIST1 argument_spec ")" OPT scope +| "[" LIST1 argument_spec "]" OPT scope +| "{" LIST1 argument_spec "}" OPT scope +] + +more_implicits_block: [ +| name +| "[" LIST1 name "]" +| "{" LIST1 name "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| +] + +hint_info: [ +| "|" OPT natural OPT constr_pattern +| +] + +reserv_list: [ +| LIST1 reserv_tuple +| simple_reserv +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| LIST1 identref ":" lconstr +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global OPT univ_name_list "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." +] + +printable: [ +| "Term" smart_global OPT univ_name_list +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" OPT dirpath +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" OPT IDENT +| "Implicit" smart_global +| [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +printunivs_subgraph: [ +| "Subgraph" "(" LIST0 reference ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| LIST1 IDENT +] + +as_dirpath: [ +| OPT [ "as" dirpath ] +] + +ne_in_or_out_modules: [ +| "inside" LIST1 global +| "outside" LIST1 global +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| +] + +comment: [ +| constr +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| +] + +searchabout_query: [ +| positive_search_mark ne_string OPT scope +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| +] + +univ_name_list: [ +| "@{" LIST0 name "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr +| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING OPT STRING +| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" OPT at_level OPT constr_as_binder_kind +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT OPT at_level OPT constr_as_binder_kind +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +simple_tactic: [ +| "btauto" +| "congruence" +| "congruence" integer +| "congruence" "with" LIST1 constr +| "congruence" integer "with" LIST1 constr +| "f_equal" +| "firstorder" OPT tactic firstorder_using +| "firstorder" OPT tactic "with" LIST1 preident +| "firstorder" OPT tactic firstorder_using "with" LIST1 preident +| "gintuition" OPT tactic +| "functional" "inversion" quantified_hypothesis OPT reference (* funind plugin *) +| "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" constr +| "exact_no_check" constr +| "vm_cast_no_check" constr +| "native_cast_no_check" constr +| "casetype" constr +| "elimtype" constr +| "lapply" constr +| "transitivity" constr +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" LIST1 bindings SEP "," +| "eexists" +| "eexists" LIST1 bindings SEP "," +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" hyp +| "intro" ident "before" hyp +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" hyp +| "intro" "before" hyp +| "move" hyp "at" "top" +| "move" hyp "at" "bottom" +| "move" hyp "after" hyp +| "move" hyp "before" hyp +| "rename" LIST1 rename SEP "," +| "revert" LIST1 hyp +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" LIST0 hyp +| "clear" "-" LIST1 hyp +| "clearbody" LIST1 hyp +| "generalize" "dependent" constr +| "replace" uconstr "with" constr clause by_arg_tac +| "replace" "->" uconstr clause +| "replace" "<-" uconstr clause +| "replace" uconstr clause +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" LIST0 simple_intropattern +| "injection" destruction_arg "as" LIST0 simple_intropattern +| "einjection" "as" LIST0 simple_intropattern +| "einjection" destruction_arg "as" LIST0 simple_intropattern +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient constr +| "dependent" "rewrite" orient constr "in" hyp +| "cutrewrite" orient constr +| "cutrewrite" orient constr "in" hyp +| "decompose" "sum" constr +| "decompose" "record" constr +| "absurd" constr +| "contradiction" OPT constr_with_bindings +| "autorewrite" "with" LIST1 preident clause +| "autorewrite" "with" LIST1 preident clause "using" tactic +| "autorewrite" "*" "with" LIST1 preident clause +| "autorewrite" "*" "with" LIST1 preident clause "using" tactic +| "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" LIST1 var +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" constr +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" constr "by" tactic +| "stepl" constr +| "stepr" constr "by" tactic +| "stepr" constr +| "generalize_eqs" hyp +| "dependent" "generalize_eqs" hyp +| "generalize_eqs_vars" hyp +| "dependent" "generalize_eqs_vars" hyp +| "specialize_eqs" hyp +| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| "hresolve_core" "(" ident ":=" constr ")" "in" constr +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" hyp +| "transparent_abstract" tactic3 +| "transparent_abstract" tactic3 "using" ident +| "constr_eq" constr constr +| "constr_eq_strict" constr constr +| "constr_eq_nounivs" constr constr +| "is_evar" constr +| "has_evar" constr +| "is_var" constr +| "is_fix" constr +| "is_cofix" constr +| "is_ind" constr +| "is_constructor" constr +| "is_proj" constr +| "is_const" constr +| "shelve" +| "shelve_unifiable" +| "unshelve" tactic1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" LIST1 constr "]" constr +| "optimize_heap" +| "eassumption" +| "eexact" constr +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" OPT int_or_var auto_using hintbases +| "info_auto" OPT int_or_var auto_using hintbases +| "debug" "auto" OPT int_or_var auto_using hintbases +| "prolog" "[" LIST0 uconstr "]" int_or_var +| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "new" "auto" OPT int_or_var auto_using hintbases +| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "dfs" "eauto" OPT int_or_var auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" hyp +| "autounfold_one" hintbases +| "unify" constr constr +| "unify" constr constr "with" preident +| "convert_concl_no_check" constr +| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var +| "head_of_constr" ident constr +| "not_evar" constr +| "is_ground" constr +| "autoapply" constr "using" preident +| "autoapply" constr "with" preident +| "progress_evars" tactic +| "decide" "equality" +| "compare" constr constr +| "rewrite_strat" rewstrategy "in" hyp +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" hyp +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" hyp +| "setoid_reflexivity" +| "setoid_transitivity" constr +| "setoid_etransitivity" +| "intros" ne_intropatterns +| "intros" +| "eintros" ne_intropatterns +| "eintros" +| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "elim" constr_with_bindings_arg OPT eliminator +| "eelim" constr_with_bindings_arg OPT eliminator +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" LIST1 fixdecl +| "cofix" ident "with" LIST1 cofixdecl +| "pose" bindings_with_parameters +| "pose" constr as_name +| "epose" bindings_with_parameters +| "epose" constr as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" constr as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" constr as_name clause_dft_concl +| "remember" constr as_name eqn_ipat clause_dft_all +| "eremember" constr as_name eqn_ipat clause_dft_all +| "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "assert" constr as_ipat by_tactic +| "eassert" constr as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" constr as_ipat by_tactic +| "eenough" constr as_ipat by_tactic +| "generalize" constr +| "generalize" constr LIST1 constr +| "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ] +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ] +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" constr in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl +| "native_compute" OPT ref_or_pattern_occ clause_dft_concl +| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl +| "fold" LIST1 constr clause_dft_concl +| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" OPT string +| "finish_timing" OPT string +| "finish_timing" "(" string ")" OPT string +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" constr (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" LIST1 ident (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "rtauto" +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" ssrdoarg (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqdir ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +firstorder_using: [ +| "using" reference +| "using" reference "," LIST1 reference SEP "," +| "using" reference reference LIST0 reference +| +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| (* funind plugin *) +] + +constr_comma_sequence': [ +| constr "," constr_comma_sequence' (* funind plugin *) +| constr (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| (* funind plugin *) +] + +function_rec_definition_loc: [ +| Vernac.rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +orient: [ +| "->" +| "<-" +| +] + +occurrences: [ +| LIST1 integer +| var +] + +glob: [ +| constr +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| constr +] + +hloc: [ +| +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" tactic3 +| +] + +in_clause: [ +| in_clause' +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," +] + +test_lpar_id_colon: [ +| local_test_lpar_id_colon +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" LIST1 preident +| +] + +auto_using: [ +| "using" LIST1 uconstr SEP "," +| +] + +hints_path_atom: [ +| LIST1 global +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" LIST1 preident +| +] + +debug: [ +| "debug" +| +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| +] + +tactic_then_last: [ +| "|" LIST0 ( OPT tactic_expr5 ) SEP "|" +| +] + +tactic_then_gen: [ +| tactic_expr5 "|" tactic_then_gen +| tactic_expr5 ".." tactic_then_last +| ".." tactic_then_last +| tactic_expr5 +| "|" tactic_then_gen +| +] + +tactic_then_locality: [ +| "[" OPT ">" +] + +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] + +tactic_expr4: [ +| tactic_expr3 ";" binder_tactic +| tactic_expr3 ";" tactic_expr3 +| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]" +| tactic_expr3 +| tactic_expr5 ";" "first" ssr_first_else (* ssr plugin *) +| tactic_expr5 ";" "first" ssrseqarg (* ssr plugin *) +| tactic_expr5 ";" "last" ssrseqarg (* ssr plugin *) +] + +tactic_expr3: [ +| "try" tactic_expr3 +| "do" int_or_var tactic_expr3 +| "timeout" int_or_var tactic_expr3 +| "time" OPT string tactic_expr3 +| "repeat" tactic_expr3 +| "progress" tactic_expr3 +| "once" tactic_expr3 +| "exactly_once" tactic_expr3 +| "infoH" tactic_expr3 +| "abstract" tactic_expr2 +| "abstract" tactic_expr2 "using" ident +| selector tactic_expr3 +| tactic_expr2 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +] + +tactic_expr2: [ +| tactic_expr1 "+" binder_tactic +| tactic_expr1 "+" tactic_expr2 +| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 +| tactic_expr1 "||" binder_tactic +| tactic_expr1 "||" tactic_expr2 +| tactic_expr1 +] + +tactic_expr1: [ +| match_key "goal" "with" match_context_list "end" +| match_key "reverse" "goal" "with" match_context_list "end" +| match_key tactic_expr5 "with" match_list "end" +| "first" "[" LIST0 tactic_expr5 SEP "|" "]" +| "solve" "[" LIST0 tactic_expr5 SEP "|" "]" +| "idtac" LIST0 message_token +| failkw [ int_or_var | ] LIST0 message_token +| simple_tactic +| tactic_arg +| reference LIST0 tactic_arg_compat +| tactic_expr0 +| tactic_expr5 ssrintros_ne (* ssr plugin *) +] + +tactic_expr0: [ +| "(" tactic_expr5 ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +failkw: [ +| "fail" +| "gfail" +] + +binder_tactic: [ +| "fun" LIST1 input_fun "=>" tactic_expr5 +| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| "info" tactic_expr5 +] + +tactic_arg_compat: [ +| tactic_arg +| Constr.constr +| "()" +] + +tactic_arg: [ +| constr_eval +| "fresh" LIST0 fresh_id +| "type_term" uconstr +| "numgoals" +] + +fresh_id: [ +| STRING +| qualid +] + +constr_eval: [ +| "eval" red_expr "in" Constr.constr +| "context" identref "[" Constr.lconstr "]" +| "type" "of" Constr.constr +] + +constr_may_eval: [ +| constr_eval +| Constr.constr +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +input_fun: [ +| "_" +| ident +] + +let_clause: [ +| identref ":=" tactic_expr5 +| "_" ":=" tactic_expr5 +| identref LIST1 input_fun ":=" tactic_expr5 +] + +match_pattern: [ +| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]" +| Constr.lconstr_pattern +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" "[" match_pattern "]" ":" match_pattern +| name ":=" match_pattern +] + +match_context_rule: [ +| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 +| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_context_list: [ +| LIST1 match_context_rule SEP "|" +| "|" LIST1 match_context_rule SEP "|" +] + +match_rule: [ +| match_pattern "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_list: [ +| LIST1 match_rule SEP "|" +| "|" LIST1 match_rule SEP "|" +] + +message_token: [ +| identref +| STRING +| integer +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5 +| Constr.global ltac_def_kind tactic_expr5 +] + +tactic: [ +| tactic_expr5 +] + +range_selector: [ +| natural "-" natural +| natural +] + +range_selector_or_nth: [ +| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ] +| natural OPT [ "," LIST1 range_selector SEP "," ] +] + +selector_body: [ +| range_selector_or_nth +| test_bracket_ident "[" ident "]" +] + +selector: [ +| "only" selector_body ":" +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +tactic_mode: [ +| OPT toplevel_selector G_vernac.query_command +| OPT toplevel_selector "{" +| OPT ltac_selector OPT ltac_info tactic ltac_use_default +| "par" ":" OPT ltac_info tactic ltac_use_default +] + +ltac_selector: [ +| toplevel_selector +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident OPT ltac_production_sep ")" +| ident +] + +ltac_tacdef_body: [ +| tacdef_body +] + +withtac: [ +| "with" Tactic.tactic +| +] + +Constr.closed_binder: [ +| "(" Prim.name ":" Constr.lconstr "|" Constr.lconstr ")" +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" constr +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" LIST0 constr +| "eval" red_expr +| "fold" constr +] + +int_or_var: [ +| integer +| identref +] + +nat_or_var: [ +| natural +| identref +] + +id_or_meta: [ +| identref +] + +open_constr: [ +| constr +] + +uconstr: [ +| constr +] + +destruction_arg: [ +| natural +| test_lpar_id_rpar constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| constr +| constr "with" constr +| constr "at" occs_nums "with" constr +] + +occs_nums: [ +| LIST1 nat_or_var +| "-" nat_or_var LIST0 int_or_var +] + +occs: [ +| "at" occs_nums +| +] + +pattern_occ: [ +| constr occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| constr occs +] + +unfold_occ: [ +| smart_global occs +] + +intropatterns: [ +| LIST0 intropattern +] + +ne_intropatterns: [ +| LIST1 intropattern +] + +or_and_intropattern: [ +| "[" LIST1 intropatterns SEP "|" "]" +| "()" +| "(" simple_intropattern ")" +| "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")" +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropatterns "]" +] + +naming_intropattern: [ +| pattern_ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed LIST0 [ "%" operconstr0 ] +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| test_lpar_idnum_coloneq LIST1 simple_binding +| LIST1 constr +] + +constr_with_bindings: [ +| constr with_bindings +] + +with_bindings: [ +| "with" bindings +| +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" LIST1 smart_global "]" +| "[" LIST1 smart_global "]" +| +] + +strategy_flag: [ +| LIST1 red_flags +| delta_flag +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag OPT ref_or_pattern_occ +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" OPT ref_or_pattern_occ +| "native_compute" OPT ref_or_pattern_occ +| "unfold" LIST1 unfold_occ SEP "," +| "fold" LIST1 constr +| "pattern" LIST1 pattern_occ SEP "," +| IDENT +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" Prim.identref ")" (* ssr plugin *) +| "(" "value" "of" Prim.identref ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| +] + +clause_dft_all: [ +| "in" in_clause +| +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| +] + +concl_occ: [ +| "*" occs +| +] + +in_hyp_list: [ +| "in" LIST1 id_or_meta +| +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| +] + +simple_binder: [ +| name +| "(" LIST1 name ":" lconstr ")" +] + +fixdecl: [ +| "(" ident LIST0 simple_binder fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident LIST0 simple_binder ":" lconstr ")" +] + +bindings_with_parameters: [ +| check_for_coloneq "(" ident LIST0 simple_binder ":=" lconstr ")" +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| identref +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| +] + +as_name: [ +| "as" ident +| +] + +by_tactic: [ +| "by" tactic_expr3 +| +] + +rewriter: [ +| "!" constr_with_bindings_arg +| [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| LIST1 induction_clause SEP "," OPT eliminator opt_clause +] + +ring_mod: [ +| "decidable" constr (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" constr (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" LIST1 global "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" constr constr (* setoid_ring plugin *) +| "sign" constr (* setoid_ring plugin *) +| "power" constr "[" LIST1 global "]" (* setoid_ring plugin *) +| "power_tac" constr "[" tactic "]" (* setoid_ring plugin *) +| "div" constr (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" LIST1 ring_mod SEP "," ")" (* setoid_ring plugin *) +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" constr (* setoid_ring plugin *) +] + +field_mods: [ +| "(" LIST1 field_mod SEP "," ")" (* setoid_ring plugin *) +] + +ssrtacarg: [ +| tactic_expr5 (* ssr plugin *) +] + +ssrtac3arg: [ +| tactic_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| test_ssrslashnum11 "/" natural "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" "=" (* ssr plugin *) +| test_ssrslashnum01 "//" natural "=" (* ssr plugin *) +| test_ssrslashnum00 "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural LIST0 natural (* ssr plugin *) +| "-" LIST0 natural (* ssr plugin *) +| "+" LIST0 natural (* ssr plugin *) +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| LEFTQMARK (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +] + +ssrterm: [ +| "YouShouldNotTypeThis" constr (* ssr plugin *) +| ssrtermkind Pcoq.Constr.constr (* ssr plugin *) +] + +ast_closure_term: [ +| term_annotation constr (* ssr plugin *) +] + +ast_closure_lterm: [ +| term_annotation lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| test_ident_no_do IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" LIST0 ident "]" (* ssr plugin *) +| "[:" LIST0 ident "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| test_nohidden "[" hat "]" (* ssr plugin *) +| test_nohidden "[" ssriorpat "]" (* ssr plugin *) +| test_nohidden "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| test_ssrfwdid Prim.ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrposefwd: [ +| LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* ssr plugin *) +] + +ssrdoarg: [ +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg OPT ssrorelse (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| tactic_expr3 (* ssr plugin *) +] + +ssrseqidx: [ +| test_ssrseqvar Prim.ident (* ssr plugin *) +| Prim.natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" tactic_expr2 (* ssr plugin *) +] + +Prim.ident: [ +| IDENT ssr_null_entry (* ssr plugin *) +] + +ssrparentacarg: [ +| "(" tactic_expr5 ")" (* ssr plugin *) +] + +ssrdotac: [ +| tactic_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssrseqdir: [ +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" LIST0 tactic_expr5 SEP "|" "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| test_ssreqid ssreqpat (* ssr plugin *) +| test_ssreqid (* ssr plugin *) +] + +ssreqpat: [ +| Prim.ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" LIST1 ssrhyp "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssragens: [ +| "{" LIST1 ssrhyp "}" ssrterm ssragens (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural constr ssrdgens (* ssr plugin *) +| natural constr (* ssr plugin *) +| constr ssrdgens (* ssr plugin *) +| constr (* ssr plugin *) +] + +ssrrwocc: [ +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrrule_ne: [ +| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| test_ssr_rw_syntax LIST1 ssrrwarg (* ssr plugin *) +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| LIST0 ssrunlockarg (* ssr plugin *) +] + +ssrsufffwd: [ +| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 ssrwgen "/" ast_closure_lterm (* ssr plugin *) +] + +ssr_idcomma: [ +| (* ssr plugin *) +| test_idcomma [ IDENT | "_" ] "," (* ssr plugin *) +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| (* ssr plugin *) +] + +ssr_modlocs: [ +| (* ssr plugin *) +| "in" LIST1 modloc (* ssr plugin *) +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| constr (* ssr plugin *) +| constr "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" constr (* ssrmatching plugin *) +| ssrtermkind constr (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| ssrtermkind lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +numnotoption: [ +| +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar new file mode 100644 index 000000000000..cd6e11505cbd --- /dev/null +++ b/doc/tools/docgram/orderedGrammar @@ -0,0 +1,4170 @@ +(* Defines the order to apply to editedGrammar to get productionlistGrammar. +doc_grammar will modify this file to add/remove nonterminals and productions +to match editedGrammar, which will remove comments. Not compiled into Coq *) +DOC_GRAMMAR + +global: [ +| reference +] + +constr_pattern: [ +| term +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| empty +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" universe_expr_list_comma ")" +| universe_expr +] + +universe_expr_list_comma: [ +| universe_expr_list_comma "," universe_expr +| universe_expr +] + +lconstr: [ +| operconstr200 +| lconstr +] + +term: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 appl_arg_list +| "@" global instance operconstr9_list_opt +| "@" pattern_identref ident_list +| operconstr9 +] + +appl_arg_list: [ +| appl_arg_list appl_arg +| appl_arg +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global appl_arg_list_opt ")" +| operconstr0 ".(" "@" global operconstr9_list_opt ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +appl_arg_list_opt: [ +| appl_arg_list_opt appl_arg +| empty +] + +operconstr9_list_opt: [ +| operconstr9_list_opt operconstr9 +| empty +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" ltac_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| empty +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" name_alt return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +name_alt: [ +| "(" name_list_comma_opt ")" +| "()" +] + +name_list_comma_opt: [ +| name_list_comma +| empty +] + +name_list_comma: [ +| name_list_comma "," name +| name +] + +name_list_opt: [ +| name_list_opt name +| empty +] + +name_list: [ +| name_list name +| name +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" "?" ident "]" +| "?" ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" inst_list_semi "}" +| empty +] + +inst_list_semi: [ +| inst_list_semi ";" inst +| inst +] + +instance: [ +| "@{" universe_level_list_opt "}" +| empty +] + +universe_level_list_opt: [ +| universe_level_list_opt universe_level +| empty +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" fix_decl_list "for" ident +] + +fix_decl_list: [ +| fix_decl_list "with" fix_decl +| fix_decl +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| ident binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" case_item_list_comma case_type_opt "with" branches "end" +] + +case_item_list_comma: [ +| case_item_list_comma "," case_item +| case_item +] + +case_type_opt: [ +| case_type +| empty +] + +case_item: [ +| operconstr100 as_opt in_opt +] + +as_opt2: [ +| as_opt case_type +| empty +] + +in_opt: [ +| "in" pattern200 +| empty +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| as_opt2 +] + +as_opt3: [ +| "as" dirpath +| empty +] + +branches: [ +| or_opt eqn_list_or_opt +] + +mult_pattern: [ +| pattern200_list_comma +] + +pattern200_list_comma: [ +| pattern200_list_comma "," pattern200 +| pattern200 +] + +eqn: [ +| mult_pattern_list_or "=>" lconstr +] + +mult_pattern_list_or: [ +| mult_pattern_list_or "|" mult_pattern +| mult_pattern +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| empty +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 pattern1_list +| "@" reference pattern1_list_opt +| pattern1 +] + +pattern1_list: [ +| pattern1_list pattern1 +| pattern1 +] + +pattern1_list_opt: [ +| pattern1_list_opt pattern1 +| empty +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" pattern200_list_or ")" +| NUMERAL +| string +] + +pattern200_list_or: [ +| pattern200_list_or "|" pattern200 +| pattern200 +] + +impl_ident_tail: [ +| "}" +| name_list ":" lconstr "}" +| name_list "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" ident "}" +| "{" "wf" term ident "}" +| "{" "measure" term ident_opt term_opt "}" +| "{" "struct" name "}" +| empty +] + +term_opt: [ +| term +| empty +] + +impl_name_head: [ +| empty +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| empty +] + +open_binders: [ +| name name_list_opt ":" lconstr +| name name_list_opt binders +| name ".." name +| closed_binder binders +] + +binders: [ +| binder_list_opt +] + +binder_list_opt: [ +| binder_list_opt binder +| empty +] + +binder: [ +| name +| closed_binder +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" exclam_opt operconstr200 +| name_colon exclam_opt operconstr200 +| operconstr200 +] + +type_cstr: [ +| lconstr_opt +| ":" lconstr +| empty +] + +preident: [ +| IDENT +] + +pattern_identref: [ +| "?" ident +] + +var: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string IDENT_opt +] + +IDENT_opt: [ +| "%" IDENT +| empty +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident field_list_opt +] + +field_list_opt: [ +| field_list_opt field +| empty +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| quoted_attributes_list_opt vernac +] + +quoted_attributes_list_opt: [ +| quoted_attributes_list_opt quoted_attributes +| empty +] + +quoted_attributes: [ +| "#[" attribute_list_comma_opt "]" +] + +attribute_list_comma_opt: [ +| attribute_list_comma +| empty +] + +attribute_list_comma: [ +| attribute_list_comma "," attribute +| attribute +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list_comma_opt ")" +| empty +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr with_list_opt +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" ident def_body +| cumulativity_token_opt private_token finite_token inductive_definition_list +| "Fixpoint" rec_definition_list +| "Let" "Fixpoint" rec_definition_list +| "CoFixpoint" corec_definition_list +| "Let" "CoFixpoint" corec_definition_list +| "Scheme" scheme_list +| "Combined" "Scheme" ident "from" ident_list_comma +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" ident lconstr_opt ":=" register_token +| "Universe" ident_list +| "Universes" ident_list +| "Constraint" univ_constraint_list_comma +] + +with_list_opt: [ +| with_list_opt "with" ident_decl binders ":" lconstr +| empty +] + +cumulativity_token_opt: [ +| cumulativity_token +| empty +] + +inductive_definition_list: [ +| inductive_definition_list "with" inductive_definition +| inductive_definition +] + +rec_definition_list: [ +| rec_definition_list "with" rec_definition +| rec_definition +] + +corec_definition_list: [ +| corec_definition_list "with" corec_definition +| corec_definition +] + +scheme_list: [ +| scheme_list "with" scheme +| scheme +] + +ident_list_comma: [ +| ident_list_comma "," ident +| ident +] + +univ_constraint_list_comma: [ +| univ_constraint_list_comma "," univ_constraint +| univ_constraint +] + +lconstr_opt2: [ +| ":=" lconstr +| empty +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| empty +] + +univ_constraint: [ +| universe_name lt_alt universe_name +] + +lt_alt: [ +| "<" +| "=" +| "<=" +] + +univ_decl: [ +| "@{" ident_list_opt plus_opt univ_constraint_alt +] + +plus_opt: [ +| "+" +| empty +] + +univ_constraint_alt: [ +| "|" univ_constraint_list_comma_opt plus_opt "}" +| rbrace_alt +] + +univ_constraint_list_comma_opt: [ +| univ_constraint_list_comma +| empty +] + +rbrace_alt: [ +| "}" +| bar_cbrace +] + +ident_decl: [ +| ident univ_decl_opt +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| empty +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| empty +] + +one_decl_notation: [ +| ne_lstring ":=" term IDENT_opt2 +] + +IDENT_opt2: [ +| ":" IDENT +| empty +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" one_decl_notation_list +| empty +] + +one_decl_notation_list: [ +| one_decl_notation_list decl_sep one_decl_notation +| one_decl_notation +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| empty +] + +inductive_definition: [ +| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" constructor_list_or +| ident constructor_type "|" constructor_list_or_opt +| ident constructor_type +| ident "{" record_fields "}" +| "{" record_fields "}" +| empty +] + +constructor_list_or: [ +| constructor_list_or "|" constructor +| constructor +] + +constructor_list_or_opt: [ +| constructor_list_or +| empty +] + +opt_coercion: [ +| ">" +| empty +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr lconstr_opt2 decl_notation +] + +lconstr_opt: [ +| ":" lconstr +| empty +] + +scheme: [ +| scheme_kind +| ident ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| quoted_attributes_list_opt record_binder natural_opt2 decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| assum_coe_list +| simple_assum_coe +] + +assum_coe_list: [ +| assum_coe_list assum_coe +| assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| ident_decl_list of_type_with_opt_coercion lconstr +] + +ident_decl_list: [ +| ident_decl_list ident_decl +| ident_decl +] + +constructor_type: [ +| binders of_type_with_opt_coercion_opt +] + +of_type_with_opt_coercion_opt: [ +| of_type_with_opt_coercion lconstr +| empty +] + +constructor: [ +| ident constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr +| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type +| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl +| "Section" ident +| "Chapter" ident +| "End" ident +| "Collection" ident ":=" section_subset_expr +| "Require" export_token global_list +| "From" global "Require" export_token global_list +| "Import" global_list +| "Export" global_list +| "Include" module_type_inl ext_module_expr_list_opt +| "Include" "Type" module_type_inl ext_module_type_list_opt +| "Transparent" smart_global_list +| "Opaque" smart_global_list +| "Strategy" strategy_level_list +| "Canonical" Structure_opt global univ_decl_opt2 +| "Canonical" Structure_opt by_notation +| "Coercion" global univ_decl_opt def_body +| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" binder_list +| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt +| "Existing" "Instance" global hint_info +| "Existing" "Instances" global_list natural_opt2 +| "Existing" "Class" global +| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" All_alt +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +module_binder_list_opt: [ +| module_binder_list_opt module_binder +| empty +] + +ext_module_expr_list_opt: [ +| ext_module_expr_list_opt ext_module_expr +| empty +] + +ext_module_type_list_opt: [ +| ext_module_type_list_opt ext_module_type +| empty +] + +strategy_level_list: [ +| strategy_level_list strategy_level "[" smart_global_list "]" +| strategy_level "[" smart_global_list "]" +] + +Structure_opt: [ +| "Structure" +| empty +] + +univ_decl_opt: [ +| univ_decl +| empty +] + +binder_list: [ +| binder_list binder +| binder +] + +record_declaration_opt: [ +| ":=" "{" record_declaration "}" +| ":=" lconstr +| empty +] + +natural_opt: [ +| natural +| empty +] + +argument_spec_block_list_opt: [ +| argument_spec_block_list_opt argument_spec_block +| empty +] + +more_implicits_block_opt: [ +| "," more_implicits_block_list_comma +| empty +] + +more_implicits_block_list_comma: [ +| more_implicits_block_list_comma "," more_implicits_block_list_opt +| more_implicits_block_list_opt +] + +arguments_modifier_opt: [ +| ":" arguments_modifier_list_comma +| empty +] + +arguments_modifier_list_comma: [ +| arguments_modifier_list_comma "," arguments_modifier +| arguments_modifier +] + +All_alt: [ +| "All" "Variables" +| "No" "Variables" +| Variable_alt ident_list +] + +Variable_alt: [ +| "Variable" +| "Variables" +] + +more_implicits_block_list_opt: [ +| more_implicits_block_list_opt more_implicits_block +| empty +] + +univ_decl_opt2: [ +| univ_decl_opt def_body +| empty +] + +export_token: [ +| "Import" +| "Export" +| empty +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| check_module_type_list_opt +] + +check_module_type_list_opt: [ +| check_module_type_list_opt check_module_type +| empty +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl ext_module_type_list_opt +| empty +] + +is_module_expr: [ +| ":=" module_expr_inl ext_module_expr_list_opt +| empty +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| empty +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token ident_list ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid univ_decl_opt ":=" lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| starredidentref_list_opt +| ssexpr35 +] + +starredidentref_list_opt: [ +| starredidentref_list_opt starredidentref +| empty +] + +starredidentref: [ +| ident +| ident "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" starredidentref_list_opt ")" +| "(" starredidentref_list_opt ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| exclam_opt name scope_opt +] + +exclam_opt: [ +| "!" +| empty +] + +scope_opt: [ +| scope +| empty +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" argument_spec_list ")" scope_opt +| "[" argument_spec_list "]" scope_opt +| "{" argument_spec_list "}" scope_opt +] + +argument_spec_list: [ +| argument_spec_list argument_spec +| argument_spec +] + +more_implicits_block: [ +| name +| "[" name_list "]" +| "{" name_list "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| empty +] + +hint_info: [ +| "|" natural_opt constr_pattern_opt +| empty +] + +reserv_list: [ +| reserv_tuple_list +| simple_reserv +] + +reserv_tuple_list: [ +| reserv_tuple_list reserv_tuple +| reserv_tuple +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| ident_list ":" lconstr +] + +command: [ +| "Comments" comment_list_opt +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" Verbose_opt ne_string_alt +| "Declare" "ML" "Module" ne_string_list +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global univ_name_list_opt +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT option_ref_value_list +| "Add" IDENT option_ref_value_list +| "Test" option_table "for" option_ref_value_list +| "Test" option_table +| "Remove" IDENT IDENT option_ref_value_list +| "Remove" IDENT option_ref_value_list +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" ident +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" ident +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" ident +| "Defined" +| "Defined" ident +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT discriminated_opt +| "Remove" "Hints" global_list opt_hintbases +| "Hint" hint opt_hintbases +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Hint" "Rewrite" orient term_list ":" preident_list_opt +| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt +| "Hint" "Rewrite" orient term_list +| "Hint" "Rewrite" orient term_list "using" tactic +| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" term +| "Derive" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Inversion" ident "with" term +| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family +| "Declare" "Left" "Step" term +| "Declare" "Right" "Step" term +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" term term +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" reference_list_opt +| "Typeclasses" "Opaque" reference_list_opt +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Setoid" term term term "as" ident +| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident +| "Add" "Morphism" term ":" ident +| "Declare" "Morphism" term ":" ident +| "Add" "Morphism" term "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Proof" "with" tactic using_opt +| "Proof" "using" section_subset_expr with_opt +| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" ltac_tacdef_body_list +| "Print" "Ltac" "Signatures" +| "String" "Notation" reference reference reference ":" ident +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Derive" ident "SuchThat" term "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" global_list (* extraction plugin *) +| "Extraction" string global_list (* extraction plugin *) +| "Extraction" "TestCompile" global_list (* extraction plugin *) +| "Separate" "Extraction" global_list (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" global_list (* extraction plugin *) +| "Extraction" "NoInline" global_list (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" int_or_id_list_opt "]" (* extraction plugin *) +| "Extraction" "Blacklist" ident_list (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global string_list_opt "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Function" function_rec_definition_loc_list (* funind plugin *) +| "Functional" "Scheme" fun_scheme_arg_list (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Add" "Ring" ident ":" term ring_mods_opt (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" term field_mods_opt (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" global_list (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc ssrhintref_list (* ssr plugin *) +] + +comment_list_opt: [ +| comment_list_opt comment +| empty +] + +Verbose_opt: [ +| "Verbose" +| empty +] + +ne_string_alt: [ +| ne_string +| IDENT +] + +ne_string_list: [ +| ne_string_list ne_string +| ne_string +] + +univ_name_list_opt: [ +| univ_name_list +| empty +] + +option_ref_value_list: [ +| option_ref_value_list option_ref_value +| option_ref_value +] + +discriminated_opt: [ +| "discriminated" +| empty +] + +global_list: [ +| global_list global +| global +] + +preident_list_opt: [ +| preident_list_opt preident +| empty +] + +reference_list_opt: [ +| reference_list_opt reference +| empty +] + +int_opt: [ +| int +| empty +] + +using_opt: [ +| "using" section_subset_expr +| empty +] + +with_opt: [ +| "with" tactic +| empty +] + +ltac_tactic_level_opt: [ +| ltac_tactic_level +| empty +] + +ltac_production_item_list: [ +| ltac_production_item_list ltac_production_item +| ltac_production_item +] + +ltac_tacdef_body_list: [ +| ltac_tacdef_body_list "with" ltac_tacdef_body +| ltac_tacdef_body +] + +int_or_id_list_opt: [ +| int_or_id_list_opt int_or_id +| empty +] + +ident_list: [ +| ident_list ident +| ident +] + +string_list_opt: [ +| string_list_opt string +| empty +] + +mlname_list_opt: [ +| mlname_list_opt mlname +| empty +] + +string_opt: [ +| string +| empty +] + +function_rec_definition_loc_list: [ +| function_rec_definition_loc_list "with" function_rec_definition_loc +| function_rec_definition_loc +] + +fun_scheme_arg_list: [ +| fun_scheme_arg_list "with" fun_scheme_arg +| fun_scheme_arg +] + +ring_mods_opt: [ +| ring_mods +| empty +] + +field_mods_opt: [ +| field_mods +| empty +] + +ssrhintref_list: [ +| ssrhintref_list ssrhintref +| ssrhintref +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global univ_name_list_opt "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "." +] + +searchabout_query_list: [ +| searchabout_query_list searchabout_query +| searchabout_query +] + +printable: [ +| "Term" smart_global univ_name_list_opt +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" dirpath_opt +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" IDENT_opt3 +| "Implicit" smart_global +| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +dirpath_opt: [ +| dirpath +| empty +] + +IDENT_opt3: [ +| IDENT +| empty +] + +Sorted_opt: [ +| "Sorted" +| empty +] + +printunivs_subgraph_opt: [ +| printunivs_subgraph +| empty +] + +ne_string_opt: [ +| ne_string +| empty +] + +printunivs_subgraph: [ +| "Subgraph" "(" reference_list_opt ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| empty +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| IDENT_list +] + +as_dirpath: [ +| as_opt3 +] + +as_opt: [ +| "as" name +| empty +] + +ne_in_or_out_modules: [ +| "inside" global_list +| "outside" global_list +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| empty +] + +comment: [ +| term +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| empty +] + +searchabout_query: [ +| positive_search_mark ne_string scope_opt +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| empty +] + +univ_name_list: [ +| "@{" name_list_opt "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" class_rawexpr_list +| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Notation" ident ident_list_opt ":=" term only_parsing +| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring syntax_modifier_opt +| "Reserved" "Notation" ne_lstring syntax_modifier_opt +] + +class_rawexpr_list: [ +| class_rawexpr_list class_rawexpr +| class_rawexpr +] + +syntax_modifier_opt: [ +| "(" syntax_modifier_list_comma ")" +| empty +] + +syntax_modifier_list_comma: [ +| syntax_modifier_list_comma "," syntax_modifier +| syntax_modifier +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| empty +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING STRING_opt +| IDENT; "," IDENT_list_comma "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +STRING_opt: [ +| STRING +| empty +] + +IDENT_list_comma: [ +| IDENT_list_comma "," IDENT +| IDENT +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" at_level_opt constr_as_binder_kind_opt +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT at_level_opt constr_as_binder_kind_opt +] + +at_level_opt: [ +| at_level +| empty +] + +constr_as_binder_kind_opt: [ +| constr_as_binder_kind +| empty +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +opt_hintbases: [ +| empty +| ":" IDENT_list +] + +IDENT_list: [ +| IDENT_list IDENT +| IDENT +] + +reference_or_constr: [ +| global +| term +] + +hint: [ +| "Resolve" reference_or_constr_list hint_info +| "Resolve" "->" global_list natural_opt +| "Resolve" "<-" global_list natural_opt +| "Immediate" reference_or_constr_list +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" global_list +| "Opaque" global_list +| "Mode" global mode +| "Unfold" global_list +| "Constructors" global_list +| "Extern" natural constr_pattern_opt "=>" tactic +] + +reference_or_constr_list: [ +| reference_or_constr_list reference_or_constr +| reference_or_constr +] + +natural_opt2: [ +| "|" natural +| empty +] + +constr_pattern_opt: [ +| constr_pattern +| empty +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| plus_list +] + +plus_list: [ +| plus_list plus_alt +| plus_alt +] + +plus_alt: [ +| "+" +| "!" +| "-" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| "Show" "Goal" natural "at" natural "." +| vernac_control +] + +orient: [ +| "->" +| "<-" +| empty +] + +occurrences: [ +| integer_list +| var +] + +integer_list: [ +| integer_list integer +| integer +] + +glob: [ +| term +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| term +] + +hloc: [ +| empty +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" ltac_expr3 +| empty +] + +in_clause: [ +| in_clause +| "*" occs +| "*" "|-" concl_occ +| hypident_occ_list_comma_opt "|-" concl_occ +| hypident_occ_list_comma_opt +] + +hypident_occ_list_comma_opt: [ +| hypident_occ_list_comma +| empty +] + +hypident_occ_list_comma: [ +| hypident_occ_list_comma "," hypident_occ +| hypident_occ +] + +test_lpar_id_colon: [ +| empty +] + +withtac: [ +| "with" tactic +| empty +] + +closed_binder: [ +| "(" name name_list ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name name_list ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name name_list "}" +| "`(" typeclass_constraint_list_comma ")" +| "`{" typeclass_constraint_list_comma "}" +| "'" pattern0 +| of_alt operconstr99 (* ssr plugin *) +| "(" "_" ":" lconstr "|" lconstr ")" +] + +typeclass_constraint_list_comma: [ +| typeclass_constraint_list_comma "," typeclass_constraint +| typeclass_constraint +] + +of_alt: [ +| "of" +| "&" +] + +simple_tactic: [ +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" term +| "exact_no_check" term +| "vm_cast_no_check" term +| "native_cast_no_check" term +| "casetype" term +| "elimtype" term +| "lapply" term +| "transitivity" term +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" bindings_list_comma +| "eexists" +| "eexists" bindings_list_comma +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" var +| "intro" ident "before" var +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" var +| "intro" "before" var +| "move" var "at" "top" +| "move" var "at" "bottom" +| "move" var "after" var +| "move" var "before" var +| "rename" rename_list_comma +| "revert" var_list +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" var_list_opt +| "clear" "-" var_list +| "clearbody" var_list +| "generalize" "dependent" term +| "replace" uconstr "with" term clause_dft_concl by_arg_tac +| "replace" "->" uconstr clause_dft_concl +| "replace" "<-" uconstr clause_dft_concl +| "replace" uconstr clause_dft_concl +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" simple_intropattern_list_opt +| "injection" destruction_arg "as" simple_intropattern_list_opt +| "einjection" "as" simple_intropattern_list_opt +| "einjection" destruction_arg "as" simple_intropattern_list_opt +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient term +| "dependent" "rewrite" orient term "in" var +| "cutrewrite" orient term +| "cutrewrite" orient term "in" var +| "decompose" "sum" term +| "decompose" "record" term +| "absurd" term +| "contradiction" constr_with_bindings_opt +| "autorewrite" "with" preident_list clause_dft_concl +| "autorewrite" "with" preident_list clause_dft_concl "using" tactic +| "autorewrite" "*" "with" preident_list clause_dft_concl +| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic +| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac +| "rewrite" "*" orient uconstr "in" var by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" var_list +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" term +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" term "by" tactic +| "stepl" term +| "stepr" term "by" tactic +| "stepr" term +| "generalize_eqs" var +| "dependent" "generalize_eqs" var +| "generalize_eqs_vars" var +| "dependent" "generalize_eqs_vars" var +| "specialize_eqs" var +| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term +| "hresolve_core" "(" ident ":=" term ")" "in" term +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" var +| "transparent_abstract" ltac_expr3 +| "transparent_abstract" ltac_expr3 "using" ident +| "constr_eq" term term +| "constr_eq_strict" term term +| "constr_eq_nounivs" term term +| "is_evar" term +| "has_evar" term +| "is_var" term +| "is_fix" term +| "is_cofix" term +| "is_ind" term +| "is_constructor" term +| "is_proj" term +| "is_const" term +| "shelve" +| "shelve_unifiable" +| "unshelve" ltac_expr1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" term_list "]" term +| "optimize_heap" +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" string_opt +| "finish_timing" string_opt +| "finish_timing" "(" string ")" string_opt +| "eassumption" +| "eexact" term +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" int_or_var_opt auto_using hintbases +| "info_auto" int_or_var_opt auto_using hintbases +| "debug" "auto" int_or_var_opt auto_using hintbases +| "prolog" "[" uconstr_list_opt "]" int_or_var +| "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "new" "auto" int_or_var_opt auto_using hintbases +| "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "dfs" "eauto" int_or_var_opt auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" var +| "autounfold_one" hintbases +| "unify" term term +| "unify" term term "with" preident +| "convert_concl_no_check" term +| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt +| "head_of_constr" ident term +| "not_evar" term +| "is_ground" term +| "autoapply" term "using" preident +| "autoapply" term "with" preident +| "progress_evars" tactic +| "rewrite_strat" rewstrategy "in" var +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" var +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" var +| "setoid_reflexivity" +| "setoid_transitivity" term +| "setoid_etransitivity" +| "decide" "equality" +| "compare" term term +| "intros" intropattern_list_opt +| "eintros" intropattern_list_opt +| "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "elim" constr_with_bindings_arg eliminator_opt +| "eelim" constr_with_bindings_arg eliminator_opt +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" fixdecl_list +| "cofix" ident "with" cofixdecl_list +| "pose" bindings_with_parameters +| "pose" term as_name +| "epose" bindings_with_parameters +| "epose" term as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" term as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" term as_name clause_dft_concl +| "remember" term as_name eqn_ipat clause_dft_all +| "eremember" term as_name eqn_ipat clause_dft_all +| "assert" "(" ident ":=" lconstr ")" +| "eassert" "(" ident ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "assert" term as_ipat by_tactic +| "eassert" term as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" term as_ipat by_tactic +| "eenough" term as_ipat by_tactic +| "generalize" term +| "generalize" term term_list +| "generalize" term occs as_name pattern_occ_list_opt +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "erewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "dependent" simple_alt quantified_hypothesis as_or_and_ipat with_opt2 +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" term in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" ref_or_pattern_occ_opt clause_dft_concl +| "native_compute" ref_or_pattern_occ_opt clause_dft_concl +| "unfold" unfold_occ_list_comma clause_dft_concl +| "fold" term_list clause_dft_concl +| "pattern" pattern_occ_list_comma clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "btauto" +| "rtauto" +| "congruence" +| "congruence" integer +| "congruence" "with" term_list +| "congruence" integer "with" term_list +| "f_equal" +| "firstorder" tactic_opt firstorder_using +| "firstorder" tactic_opt "with" preident_list +| "firstorder" tactic_opt firstorder_using "with" preident_list +| "gintuition" tactic_opt +| "functional" "inversion" quantified_hypothesis reference_opt (* funind plugin *) +| "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" term (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" ident_list (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "field_lookup" tactic "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +var_list: [ +| var_list var +| var +] + +var_list_opt: [ +| var_list_opt var +| empty +] + +constr_with_bindings_opt: [ +| constr_with_bindings +| empty +] + +int_or_var_opt: [ +| int_or_var +| empty +] + +uconstr_list_opt: [ +| uconstr_list_opt uconstr +| empty +] + +constr_with_bindings_arg_list_comma: [ +| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg +| constr_with_bindings_arg +] + +fixdecl_list: [ +| fixdecl_list fixdecl +| fixdecl +] + +cofixdecl_list: [ +| cofixdecl_list cofixdecl +| cofixdecl +] + +pattern_occ_list_opt: [ +| pattern_occ_list_opt "," pattern_occ as_name +| empty +] + +oriented_rewriter_list_comma: [ +| oriented_rewriter_list_comma "," oriented_rewriter +| oriented_rewriter +] + +simple_alt: [ +| "simple" "inversion" +| "inversion" +| "inversion_clear" +] + +with_opt2: [ +| "with" term +| empty +] + +tactic_opt: [ +| tactic +| empty +] + +reference_opt: [ +| reference +| empty +] + +bindings_list_comma: [ +| bindings_list_comma "," bindings +| bindings +] + +rename_list_comma: [ +| rename_list_comma "," rename +| rename +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" preident_list +| empty +] + +preident_list: [ +| preident_list preident +| preident +] + +auto_using: [ +| "using" uconstr_list_comma +| empty +] + +uconstr_list_comma: [ +| uconstr_list_comma "," uconstr +| uconstr +] + +hints_path_atom: [ +| global_list +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" preident_list +| empty +] + +debug: [ +| "debug" +| empty +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| empty +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" term +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" term_list_opt +| "eval" red_expr +| "fold" term +] + +term_list_opt: [ +| term_list_opt term +| empty +] + +int_or_var: [ +| integer +| ident +] + +nat_or_var: [ +| natural +| ident +] + +id_or_meta: [ +| ident +] + +open_constr: [ +| term +] + +uconstr: [ +| term +] + +destruction_arg: [ +| natural +| constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| term +| term "with" term +| term "at" occs_nums "with" term +] + +occs_nums: [ +| nat_or_var_list +| "-" nat_or_var int_or_var_list_opt +] + +nat_or_var_list: [ +| nat_or_var_list nat_or_var +| nat_or_var +] + +int_or_var_list_opt: [ +| int_or_var_list_opt int_or_var +| empty +] + +occs: [ +| "at" occs_nums +| empty +] + +pattern_occ: [ +| term occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| term occs +] + +unfold_occ: [ +| smart_global occs +] + +intropattern_list_opt: [ +| intropattern_list_opt intropattern +| empty +] + +or_and_intropattern: [ +| "[" intropattern_or_list_or "]" +| "(" simple_intropattern_list_comma_opt ")" +| "(" simple_intropattern "&" simple_intropattern_list_ ")" +] + +simple_intropattern_list_comma_opt: [ +| simple_intropattern_list_comma +| empty +] + +simple_intropattern_list_comma: [ +| simple_intropattern_list_comma "," simple_intropattern +| simple_intropattern +] + +simple_intropattern_list_: [ +| simple_intropattern_list_ "&" simple_intropattern +| simple_intropattern +] + +intropattern_or_list_or: [ +| intropattern_or_list_or "|" intropattern_list_opt +| intropattern_list_opt +] + +simple_intropattern_list_opt: [ +| simple_intropattern_list_opt simple_intropattern +| empty +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropattern_list_opt "]" +] + +naming_intropattern: [ +| "?" ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed operconstr0_list_opt +] + +operconstr0_list_opt: [ +| operconstr0_list_opt "%" operconstr0 +| empty +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| simple_binding_list +| term_list +] + +simple_binding_list: [ +| simple_binding_list simple_binding +| simple_binding +] + +term_list: [ +| term_list term +| term +] + +constr_with_bindings: [ +| term with_bindings +] + +with_bindings: [ +| "with" bindings +| empty +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" smart_global_list "]" +| "[" smart_global_list "]" +| empty +] + +smart_global_list: [ +| smart_global_list smart_global +| smart_global +] + +strategy_flag: [ +| red_flags_list +| delta_flag +] + +red_flags_list: [ +| red_flags_list red_flags +| red_flags +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag ref_or_pattern_occ_opt +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" ref_or_pattern_occ_opt +| "native_compute" ref_or_pattern_occ_opt +| "unfold" unfold_occ_list_comma +| "fold" term_list +| "pattern" pattern_occ_list_comma +| IDENT +] + +ref_or_pattern_occ_opt: [ +| ref_or_pattern_occ +| empty +] + +unfold_occ_list_comma: [ +| unfold_occ_list_comma "," unfold_occ +| unfold_occ +] + +pattern_occ_list_comma: [ +| pattern_occ_list_comma "," pattern_occ +| pattern_occ +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" ident ")" (* ssr plugin *) +| "(" "value" "of" ident ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| empty +] + +clause_dft_all: [ +| "in" in_clause +| empty +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| empty +] + +concl_occ: [ +| "*" occs +| empty +] + +in_hyp_list: [ +| "in" id_or_meta_list +| empty +] + +id_or_meta_list: [ +| id_or_meta_list id_or_meta +| id_or_meta +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| empty +] + +simple_binder: [ +| name +| "(" name_list ":" lconstr ")" +] + +fixdecl: [ +| "(" ident simple_binder_list_opt fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident simple_binder_list_opt ":" lconstr ")" +] + +bindings_with_parameters: [ +| "(" ident simple_binder_list_opt ":=" lconstr ")" +] + +simple_binder_list_opt: [ +| simple_binder_list_opt simple_binder +| empty +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| empty +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| ident +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| empty +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| empty +] + +as_name: [ +| "as" ident +| empty +] + +by_tactic: [ +| "by" ltac_expr3 +| empty +] + +rewriter: [ +| "!" constr_with_bindings_arg +| qmark_alt constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural qmark_alt constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +qmark_alt: [ +| "?" +| "?" +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| induction_clause_list_comma eliminator_opt opt_clause +] + +induction_clause_list_comma: [ +| induction_clause_list_comma "," induction_clause +| induction_clause +] + +eliminator_opt: [ +| eliminator +| empty +] + +ltac_expr: [ +| binder_tactic +| ltac_expr4 +] + +binder_tactic: [ +| "fun" input_fun_list "=>" ltac_expr +| "let" rec_opt let_clause_list "in" ltac_expr +| "info" ltac_expr +] + +input_fun_list: [ +| input_fun_list input_fun +| input_fun +] + +input_fun: [ +| "_" +| ident +] + +rec_opt: [ +| "rec" +| empty +] + +let_clause_list: [ +| let_clause_list "with" let_clause +| let_clause +] + +let_clause: [ +| ident ":=" ltac_expr +| "_" ":=" ltac_expr +| ident input_fun_list ":=" ltac_expr +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]" +| ltac_expr3 +| ltac_expr ";" "first" ssr_first_else (* ssr plugin *) +| ltac_expr ";" "first" ssrseqarg (* ssr plugin *) +| ltac_expr ";" "last" ssrseqarg (* ssr plugin *) +] + +gt_opt: [ +| ">" +| empty +] + +tactic_then_gen: [ +| ltac_expr_opt "|" tactic_then_gen +| ltac_expr_opt ".." or_opt ltac_expr_list2 +| ltac_expr +| empty +] + +ltac_expr_opt: [ +| ltac_expr +| empty +] + +ltac_expr_list_or2_opt: [ +| ltac_expr_list_or2 +| empty +] + +ltac_expr_list_or2: [ +| ltac_expr_list_or2 "|" ltac_expr_opt +| ltac_expr_opt +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" string_opt ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| selector ltac_expr3 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| ltac_expr2 +] + +tactic_mode: [ +| toplevel_selector_opt query_command +| toplevel_selector_opt "{" +| toplevel_selector_opt ltac_info_opt tactic ltac_use_default +| "par" ":" ltac_info_opt tactic ltac_use_default +] + +toplevel_selector_opt: [ +| toplevel_selector +| empty +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +selector: [ +| "only" selector_body ":" +] + +selector_body: [ +| range_selector_list_comma +| "[" ident "]" +] + +range_selector_list_comma: [ +| range_selector_list_comma "," range_selector +| range_selector +] + +range_selector: [ +| natural "-" natural +| natural +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ +| match_key reverse_opt "goal" "with" match_context_list "end" +| match_key ltac_expr "with" match_list "end" +| "first" "[" ltac_expr_list_or_opt "]" +| "solve" "[" ltac_expr_list_or_opt "]" +| "idtac" message_token_list_opt +| failkw int_or_var_opt message_token_list_opt +| simple_tactic +| tactic_arg +| reference tactic_arg_compat_list_opt +| ltac_expr ssrintros_ne (* ssr plugin *) +| ltac_expr0 +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +reverse_opt: [ +| "reverse" +| empty +] + +ltac_expr_list_or_opt: [ +| ltac_expr_list_or +| empty +] + +ltac_expr_list_or: [ +| ltac_expr_list_or "|" ltac_expr +| ltac_expr +] + +match_context_list: [ +| or_opt match_context_rule_list_or +] + +match_context_rule_list_or: [ +| match_context_rule_list_or "|" match_context_rule +| match_context_rule +] + +or_opt: [ +| "|" +| empty +] + +eqn_list_or_opt: [ +| eqn_list_or +| empty +] + +eqn_list_or: [ +| eqn_list_or "|" eqn +| eqn +] + +match_context_rule: [ +| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr +| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr +| "_" "=>" ltac_expr +] + +match_hyps_list_comma_opt: [ +| match_hyps_list_comma +| empty +] + +match_hyps_list_comma: [ +| match_hyps_list_comma "," match_hyps +| match_hyps +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" match_pattern_opt match_pattern +] + +match_pattern: [ +| "context" ident_opt "[" lconstr_pattern "]" +| lconstr_pattern +] + +ident_opt: [ +| ident +| empty +] + +lconstr_pattern: [ +| lconstr +] + +match_pattern_opt: [ +| "[" match_pattern "]" ":" +| empty +] + +match_list: [ +| or_opt match_rule_list_or +] + +match_rule_list_or: [ +| match_rule_list_or "|" match_rule +| match_rule +] + +match_rule: [ +| match_pattern "=>" ltac_expr +| "_" "=>" ltac_expr +] + +message_token_list_opt: [ +| message_token_list_opt message_token +| empty +] + +message_token: [ +| ident +| STRING +| integer +] + +failkw: [ +| "fail" +| "gfail" +] + +tactic_arg: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| "fresh" fresh_id_list_opt +| "type_term" uconstr +| "numgoals" +] + +fresh_id_list_opt: [ +| fresh_id_list_opt fresh_id +| empty +] + +fresh_id: [ +| STRING +| qualid +] + +tactic_arg_compat_list_opt: [ +| tactic_arg_compat_list_opt tactic_arg_compat +| empty +] + +tactic_arg_compat: [ +| tactic_arg +| term +| "()" +] + +ltac_expr0: [ +| "(" ltac_expr ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +constr_may_eval: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| term +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| global input_fun_list ltac_def_kind ltac_expr +| global ltac_def_kind ltac_expr +] + +tactic: [ +| ltac_expr +] + +ltac_info_opt: [ +| ltac_info +| empty +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident ltac_production_sep_opt ")" +| ident +] + +ltac_production_sep_opt: [ +| ltac_production_sep +| empty +] + +ltac_tacdef_body: [ +| tacdef_body +] + +firstorder_using: [ +| "using" reference +| "using" reference "," reference_list_comma +| "using" reference reference reference_list_opt +| empty +] + +reference_list_comma: [ +| reference_list_comma "," reference +| reference +] + +numnotoption: [ +| empty +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| empty (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| empty (* funind plugin *) +] + +constr_comma_sequence': [ +| term "," constr_comma_sequence' (* funind plugin *) +| term (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| empty (* funind plugin *) +] + +function_rec_definition_loc: [ +| rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +ring_mod: [ +| "decidable" term (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" term (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" global_list "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" term term (* setoid_ring plugin *) +| "sign" term (* setoid_ring plugin *) +| "power" term "[" global_list "]" (* setoid_ring plugin *) +| "power_tac" term "[" tactic "]" (* setoid_ring plugin *) +| "div" term (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" ring_mod_list_comma ")" (* setoid_ring plugin *) +] + +ring_mod_list_comma: [ +| ring_mod_list_comma "," ring_mod +| ring_mod +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" term (* setoid_ring plugin *) +] + +field_mods: [ +| "(" field_mod_list_comma ")" (* setoid_ring plugin *) +] + +field_mod_list_comma: [ +| field_mod_list_comma "," field_mod +| field_mod +] + +ssrtacarg: [ +| ltac_expr (* ssr plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| "/" natural "/" natural "=" (* ssr plugin *) +| "/" natural "/" (* ssr plugin *) +| "/" natural "=" (* ssr plugin *) +| "/" natural "/=" (* ssr plugin *) +| "/" natural "/" "=" (* ssr plugin *) +| "//" natural "=" (* ssr plugin *) +| "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" ssrhyp_list "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural natural_list_opt (* ssr plugin *) +| "-" natural_list_opt (* ssr plugin *) +| "+" natural_list_opt (* ssr plugin *) +] + +natural_list_opt: [ +| natural_list_opt natural +| empty +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| "?" (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +] + +ssrhyp_list_opt: [ +| ssrhyp_list_opt ssrhyp +| empty +] + +ssrterm: [ +| "YouShouldNotTypeThis" term (* ssr plugin *) +| term (* ssr plugin *) +] + +ast_closure_term: [ +| term (* ssr plugin *) +] + +ast_closure_lterm: [ +| lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" term (* ssr plugin *) +| "/" term ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" ast_closure_term (* ssr plugin *) +| "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" ident_list_opt "]" (* ssr plugin *) +| "[:" ident_list_opt "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ident_list_opt: [ +| ident_list_opt ident +| empty +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| "[" hat "]" (* ssr plugin *) +| "[" ssriorpat "]" (* ssr plugin *) +| "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| empty (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ssrbvar_list ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| of_alt operconstr99 (* ssr plugin *) +] + +ssrbvar_list: [ +| ssrbvar_list ssrbvar +| ssrbvar +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrposefwd: [ +| ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrbinder_list_opt: [ +| ssrbinder_list_opt ssrbinder +| empty +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd (* ssr plugin *) +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg ssrorelse_opt (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| ltac_expr3 (* ssr plugin *) +] + +ssrorelse_opt: [ +| ssrorelse +| empty +] + +ssrseqidx: [ +| ident (* ssr plugin *) +| natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* ssr plugin *) +] + +ident: [ +| IDENT +] + +ssrparentacarg: [ +| "(" ltac_expr ")" (* ssr plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" ltac_expr_list_or_opt "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" ssrhyp_list "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| ssreqpat (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssreqpat: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" ssrhyp_list "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrhyp_list: [ +| ssrhyp_list ssrhyp +| ssrhyp +] + +ssragens: [ +| "{" ssrhyp_list "}" ssrterm ssragens (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural term ssrdgens (* ssr plugin *) +| natural term (* ssr plugin *) +| term ssrdgens (* ssr plugin *) +| term (* ssr plugin *) +] + +ssrrwocc: [ +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrrule_ne: [ +| ssrterm_alt (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrterm_alt: [ +| "/" ssrterm +| ssrterm +| ssrsimpl_ne +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| ssrrwarg_list (* ssr plugin *) +] + +ssrrwarg_list: [ +| ssrrwarg_list ssrrwarg +| ssrrwarg +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| ssrunlockarg_list_opt (* ssr plugin *) +] + +ssrunlockarg_list_opt: [ +| ssrunlockarg_list_opt ssrunlockarg +| empty +] + +ssrsufffwd: [ +| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" ssrwgen_list_opt "/" ast_closure_lterm (* ssr plugin *) +] + +ssrwgen_list_opt: [ +| ssrwgen_list_opt ssrwgen +| empty +] + +ssr_idcomma: [ +| empty (* ssr plugin *) +| IDENT_alt "," (* ssr plugin *) +] + +IDENT_alt: [ +| IDENT +| "_" +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssr_modlocs: [ +| empty (* ssr plugin *) +| "in" modloc_list (* ssr plugin *) +] + +modloc_list: [ +| modloc_list modloc +| modloc +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| term (* ssr plugin *) +| term "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" term (* ssrmatching plugin *) +| term (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +empty: [ +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" +] + +int: [ +| integer +] + +command_entry: [ +| noedit_mode +] + diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg new file mode 100644 index 000000000000..a28d07636a90 --- /dev/null +++ b/doc/tools/docgram/prodn.edit_mlg @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(*