From 0d33024ff79c38d52fde49e23d0e45d9c22eefbe Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 12 Sep 2020 20:54:22 -0700 Subject: Convert 2nd part of rewriting chapter to prodn --- doc/tools/docgram/common.edit_mlg | 42 +- doc/tools/docgram/fullGrammar | 2126 ++++++++++++++++++------------------- doc/tools/docgram/orderedGrammar | 72 +- 3 files changed, 1137 insertions(+), 1103 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 27144fd1ad..24ecc65e9b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -62,8 +62,8 @@ SPLICE: [ ] RENAME: [ -| G_LTAC2_delta_flag ltac2_delta_flag -| G_LTAC2_strategy_flag ltac2_strategy_flag +| G_LTAC2_delta_flag ltac2_delta_reductions +| G_LTAC2_strategy_flag ltac2_reductions | G_LTAC2_binder ltac2_binder | G_LTAC2_branches ltac2_branches | G_LTAC2_let_clause ltac2_let_clause @@ -640,7 +640,7 @@ delta_flag: [ | OPTINREF ] -ltac2_delta_flag: [ +ltac2_delta_reductions: [ | EDIT ADD_OPT "-" "[" refglobals "]" (* Ltac2 plugin *) ] @@ -924,6 +924,10 @@ where: [ | "before" ident ] +simple_occurrences: [ +(* placeholder (yuck) *) +] + simple_tactic: [ | REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases | WITH "eauto" OPT nat_or_var auto_using hintbases @@ -937,6 +941,26 @@ simple_tactic: [ | DELETE "autorewrite" "*" "with" LIST1 preident clause | REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic | WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic ) +| REPLACE "autounfold" hintbases clause_dft_concl +| WITH "autounfold" hintbases OPT simple_occurrences +| REPLACE "red" clause_dft_concl +| WITH "red" simple_occurrences +| REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl +| WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences +| REPLACE "hnf" clause_dft_concl +| WITH "hnf" simple_occurrences +| REPLACE "cbv" strategy_flag clause_dft_concl +| WITH "cbv" strategy_flag simple_occurrences +| PRINT +| REPLACE "compute" OPT delta_flag clause_dft_concl +| WITH "compute" OPT delta_flag simple_occurrences +| REPLACE "lazy" strategy_flag clause_dft_concl +| WITH "lazy" strategy_flag simple_occurrences +| REPLACE "cbn" strategy_flag clause_dft_concl +| WITH "cbn" strategy_flag simple_occurrences +| REPLACE "fold" LIST1 constr clause_dft_concl +| WITH "fold" LIST1 constr simple_occurrences + | DELETE "cofix" ident | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) @@ -2460,6 +2484,10 @@ clause_dft_concl: [ | WITH occs ] +simple_occurrences: [ +| clause_dft_concl (* semantically restricted: no "at" clause *) +] + occs_nums: [ | EDIT ADD_OPT "-" LIST1 nat_or_var ] @@ -2471,10 +2499,8 @@ variance_identref: [ conversion: [ | DELETE constr | DELETE constr "with" constr -| PRINT | REPLACE constr "at" occs_nums "with" constr | WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr -| PRINT ] SPLICE: [ @@ -2762,6 +2788,10 @@ RENAME: [ | hypident_occ hyp_occs | concl_occ concl_occs | constr_with_bindings_arg one_term_with_bindings +| red_flag reduction +| strategy_flag reductions +| delta_flag delta_reductions +| q_strategy_flag q_reductions ] simple_tactic: [ @@ -2806,7 +2836,7 @@ NOTINRSTS: [ | q_destruction_arg | q_with_bindings | q_bindings -| q_strategy_flag +| q_reductions | q_reference | q_clause | q_occurrences diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index bc6b803bbb..be1b9d80fb 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,1470 +1,1470 @@ (* 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 -] - -cpattern: [ -| lconstr -] - -sort: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -| "Type" "@{" "_" "}" -| "Type" "@{" universe "}" -] - -sort_family: [ -| "Set" -| "Prop" -| "SProp" -| "Type" -] - -universe_increment: [ -| "+" natural +opt_hintbases: [ | +| ":" LIST1 IDENT ] -universe_name: [ -| global -| "Set" -| "Prop" +command: [ +| "Goal" lconstr +| "Proof" +| "Proof" "using" G_vernac.section_subset_expr +| "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 ":" term200 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 +| "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 +| "Set" setting_name option_setting +| "Unset" setting_name +| "Print" "Table" setting_name +| "Add" IDENT IDENT LIST1 table_value +| "Add" IDENT LIST1 table_value +| "Test" setting_name "for" LIST1 table_value +| "Test" setting_name +| "Remove" IDENT IDENT LIST1 table_value +| "Remove" IDENT LIST1 table_value +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" identref +| "Back" +| "Back" 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_fix_definition 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" LIST1 reference +| "Typeclasses" "Opaque" LIST1 reference +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural +| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] +| "Proof" "using" G_vernac.section_subset_expr "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" natural "of" ident ":" lglob withtac +| "Obligation" natural "of" ident withtac +| "Obligation" natural ":" lglob withtac +| "Obligation" natural withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" natural "of" ident "with" tactic +| "Solve" "Obligation" natural "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "of" ident +| "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" integer +| "Show" "Ltac" "Profile" string +| "Show" "Lia" "Profile" (* micromega plugin *) +| "Add" "Zify" "InjTyp" constr (* micromega plugin *) +| "Add" "Zify" "BinOp" constr (* micromega plugin *) +| "Add" "Zify" "UnOp" constr (* micromega plugin *) +| "Add" "Zify" "CstOp" constr (* micromega plugin *) +| "Add" "Zify" "BinRel" constr (* micromega plugin *) +| "Add" "Zify" "PropOp" constr (* micromega plugin *) +| "Add" "Zify" "PropBinOp" constr (* micromega plugin *) +| "Add" "Zify" "PropUOp" constr (* micromega plugin *) +| "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) +| "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) +| "Add" "Zify" "Saturate" constr (* micromega plugin *) +| "Show" "Zify" "InjTyp" (* micromega plugin *) +| "Show" "Zify" "BinOp" (* micromega plugin *) +| "Show" "Zify" "UnOp" (* micromega plugin *) +| "Show" "Zify" "CstOp" (* micromega plugin *) +| "Show" "Zify" "BinRel" (* micromega plugin *) +| "Show" "Zify" "UnOpSpec" (* micromega plugin *) +| "Show" "Zify" "BinOpSpec" (* micromega plugin *) +| "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *) +| "Print" "Rings" (* ring plugin *) +| "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) +| "Print" "Fields" (* ring plugin *) +| "Prenex" "Implicits" LIST1 global (* SSR plugin *) +| "Print" "Hint" "View" ssrviewpos (* SSR plugin *) +| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* SSR plugin *) +| "Search" ssr_search_arg ssr_modlocs (* SSR plugin *) +| "Number" "Notation" reference reference reference OPT number_options ":" ident +| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| "String" "Notation" reference reference reference OPT string_option ":" ident +| "Ltac2" ltac2_entry (* Ltac2 plugin *) +| "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) +| "Print" "Ltac2" reference (* Ltac2 plugin *) ] -universe_expr: [ -| universe_name universe_increment +reference_or_constr: [ +| global +| constr ] -universe: [ -| "max" "(" LIST1 universe_expr SEP "," ")" -| universe_expr +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 ] -lconstr: [ -| term200 +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr ] -constr: [ -| term8 -| "@" global univ_annot +mode: [ +| LIST1 [ "+" | "!" | "-" ] ] -term200: [ -| binder_constr -| term100 +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac ] -term100: [ -| term99 "<:" term200 -| term99 "<<:" term200 -| term99 ":" term200 -| term99 ":>" -| term99 +decorated_vernac: [ +| LIST0 quoted_attributes vernac ] -term99: [ -| term90 +quoted_attributes: [ +| "#[" attribute_list "]" ] -term90: [ -| term10 +attribute_list: [ +| LIST0 attribute SEP "," ] -term10: [ -| term9 LIST1 arg -| "@" global univ_annot LIST0 term9 -| "@" pattern_ident LIST1 identref -| term9 +attribute: [ +| ident attr_value +| "using" attr_value ] -term9: [ -| ".." term0 ".." -| term8 +attr_value: [ +| "=" string +| "=" IDENT +| "(" attribute_list ")" +| ] -term8: [ -| term1 +legacy_attr: [ +| "Local" +| "Global" +| "Polymorphic" +| "Monomorphic" +| "Cumulative" +| "NonCumulative" +| "Private" +| "Program" ] -term1: [ -| term0 ".(" global LIST0 arg ")" -| term0 ".(" "@" global LIST0 ( term9 ) ")" -| term0 "%" IDENT -| term0 +vernac: [ +| LIST0 legacy_attr vernac_aux ] -term0: [ -| atomic_constr -| term_match -| "(" term200 ")" -| "{|" record_declaration bar_cbrace -| "{" binder_constr "}" -| "`{" term200 "}" -| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot -| "`(" term200 ")" -| "ltac" ":" "(" Pltac.ltac_expr ")" +vernac_aux: [ +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry ] -array_elems: [ -| LIST0 lconstr SEP ";" +noedit_mode: [ +| query_command ] -record_declaration: [ -| fields_def +subprf: [ +| BULLET +| "{" +| "}" ] -fields_def: [ -| field_def ";" fields_def -| field_def -| +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" ident_decl def_body +| finite_token LIST1 inductive_definition SEP "with" +| "Fixpoint" LIST1 fix_definition SEP "with" +| "Let" "Fixpoint" LIST1 fix_definition SEP "with" +| "CoFixpoint" LIST1 cofix_definition SEP "with" +| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" +| "Scheme" LIST1 scheme SEP "with" +| "Combined" "Scheme" identref "from" LIST1 identref SEP "," +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token +| "Universe" LIST1 identref +| "Universes" LIST1 identref +| "Constraint" LIST1 univ_constraint SEP "," ] -field_def: [ -| global binders ":=" lconstr +register_token: [ +| test_hash_ident "#" IDENT ] -binder_constr: [ -| "forall" open_binders "," term200 -| "fun" open_binders "=>" term200 -| "let" name binders let_type_cstr ":=" term200 "in" term200 -| "let" "fix" fix_decl "in" term200 -| "let" "cofix" cofix_body "in" term200 -| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 "in" term200 -| "let" "'" pattern200 ":=" term200 case_type "in" term200 -| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 -| "if" term200 as_return_type "then" term200 "else" term200 -| "fix" fix_decls -| "cofix" cofix_decls -| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) -| "if" term200 "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 *) +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" ] -arg: [ -| test_lpar_id_coloneq "(" identref ":=" lconstr ")" -| term9 +def_token: [ +| "Definition" +| "Example" +| "SubClass" ] -atomic_constr: [ -| global univ_annot -| sort -| NUMBER -| string -| "_" -| "?" "[" identref "]" -| "?" "[" pattern_ident "]" -| pattern_ident evar_instance +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" ] -inst: [ -| identref ":=" lconstr +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" ] -evar_instance: [ -| "@{" LIST1 inst SEP ";" "}" +inline: [ +| "Inline" "(" natural ")" +| "Inline" | ] -univ_annot: [ -| "@{" LIST0 universe_level "}" -| +univ_constraint: [ +| universe_name [ "<" | "=" | "<=" ] universe_name ] -universe_level: [ -| "Set" -| "Prop" -| "Type" -| "_" -| global +univ_decl: [ +| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] ] -fix_decls: [ -| fix_decl -| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref +variance: [ +| "+" +| "=" +| "*" ] -cofix_decls: [ -| cofix_body -| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref +variance_identref: [ +| identref +| test_variance_ident variance identref ] -fix_decl: [ -| identref binders_fixannot type_cstr ":=" term200 +cumul_univ_decl: [ +| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] ] -cofix_body: [ -| identref binders type_cstr ":=" term200 +ident_decl: [ +| identref OPT univ_decl ] -term_match: [ -| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +cumul_ident_decl: [ +| identref OPT cumul_univ_decl ] -case_item: [ -| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" ] -case_type: [ -| "return" term100 +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr ] -as_return_type: [ -| OPT [ OPT [ "as" name ] case_type ] +reduce: [ +| "Eval" red_expr "in" +| ] -branches: [ -| OPT "|" LIST0 eqn SEP "|" +decl_notation: [ +| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] ] -mult_pattern: [ -| LIST1 pattern200 SEP "," +decl_sep: [ +| "and" ] -eqn: [ -| LIST1 mult_pattern SEP "|" "=>" lconstr +decl_notations: [ +| "where" LIST1 decl_notation SEP decl_sep +| ] -record_pattern: [ -| global ":=" pattern200 +opt_constructors_or_fields: [ +| ":=" constructors_or_record +| ] -record_patterns: [ -| record_pattern ";" record_patterns -| record_pattern +inductive_definition: [ +| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +] + +constructors_or_record: [ +| "|" LIST1 constructor SEP "|" +| identref constructor_type "|" LIST1 constructor SEP "|" +| identref constructor_type +| identref "{" record_fields "}" +| "{" record_fields "}" | ] -pattern200: [ -| pattern100 +opt_coercion: [ +| ">" +| ] -pattern100: [ -| pattern99 ":" term200 -| pattern99 +fix_definition: [ +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] -pattern99: [ -| pattern90 +cofix_definition: [ +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] -pattern90: [ -| pattern10 +scheme: [ +| scheme_kind +| identref ":=" scheme_kind ] -pattern10: [ -| pattern1 "as" name -| pattern1 LIST1 pattern1 -| "@" Prim.reference LIST0 pattern1 -| pattern1 +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 ] -pattern1: [ -| pattern0 "%" IDENT -| pattern0 +record_field: [ +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations ] -pattern0: [ -| Prim.reference -| "{|" record_patterns bar_cbrace -| "_" -| "(" pattern200 ")" -| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" -| NUMBER -| string +record_fields: [ +| record_field ";" record_fields +| record_field +| ] -fixannot: [ -| "{" "struct" identref "}" -| "{" "wf" constr identref "}" -| "{" "measure" constr OPT identref OPT constr "}" +field_body: [ +| binders of_type lconstr +| binders of_type lconstr ":=" lconstr +| binders ":=" lconstr ] -binders_fixannot: [ -| ensure_fixannot fixannot -| binder binders_fixannot -| +record_binder: [ +| name +| name field_body ] -open_binders: [ -| name LIST0 name ":" lconstr -| name LIST0 name binders -| name ".." name -| closed_binder binders +assum_list: [ +| LIST1 assum_coe +| assumpt ] -binders: [ -| LIST0 binder -| Pcoq.Constr.binders +assum_coe: [ +| "(" assumpt ")" ] -binder: [ -| name -| closed_binder +assumpt: [ +| LIST1 ident_decl of_type lconstr ] -closed_binder: [ -| "(" name LIST1 name ":" lconstr ")" -| "(" name ":" lconstr ")" -| "(" name ":=" lconstr ")" -| "(" name ":" lconstr ":=" lconstr ")" -| "{" name "}" -| "{" name LIST1 name ":" lconstr "}" -| "{" name ":" lconstr "}" -| "{" name LIST1 name "}" -| "[" name "]" -| "[" name LIST1 name ":" lconstr "]" -| "[" name ":" lconstr "]" -| "[" name LIST1 name "]" -| "`(" LIST1 typeclass_constraint SEP "," ")" -| "`{" LIST1 typeclass_constraint SEP "," "}" -| "`[" LIST1 typeclass_constraint SEP "," "]" -| "'" pattern0 -| [ "of" | "&" ] term99 (* SSR plugin *) +constructor_type: [ +| binders [ of_type lconstr | ] ] -one_open_binder: [ -| name -| name ":" lconstr -| one_closed_binder +constructor: [ +| identref constructor_type ] -one_closed_binder: [ -| "(" name ":" lconstr ")" -| "{" name "}" -| "{" name ":" lconstr "}" -| "[" name "]" -| "[" name ":" lconstr "]" -| "'" pattern0 +of_type: [ +| ":>" +| ":" ">" +| ":" ] -typeclass_constraint: [ -| "!" term200 -| "{" name "}" ":" [ "!" | ] term200 -| test_name_colon name ":" [ "!" | ] term200 -| term200 +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 +| "End" identref +| "Collection" identref ":=" section_subset_expr +| "Require" export_token LIST1 global +| "From" global "Require" export_token LIST1 global +| "Import" LIST1 filtered_import +| "Export" LIST1 filtered_import +| "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 ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Existing" "Instance" global hint_info +| "Existing" "Instances" LIST1 global OPT [ "|" natural ] +| "Existing" "Class" global +| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] +| "Export" "Set" setting_name option_setting +| "Export" "Unset" setting_name +| "Import" "Prenex" "Implicits" (* SSR plugin *) ] -type_cstr: [ -| ":" lconstr -| +filtered_import: [ +| global +| global "(" LIST1 one_import_filter_name SEP "," ")" ] -let_type_cstr: [ -| OPT [ ":" lconstr ] +one_import_filter_name: [ +| global OPT [ "(" ".." ")" ] ] -preident: [ -| IDENT +export_token: [ +| "Import" +| "Export" +| ] -ident: [ -| IDENT +ext_module_type: [ +| "<+" module_type_inl ] -pattern_ident: [ -| LEFTQMARK ident +ext_module_expr: [ +| "<+" module_expr_inl ] -identref: [ -| ident +check_module_type: [ +| "<:" module_type_inl ] -hyp: [ -| identref +check_module_types: [ +| LIST0 check_module_type ] -field: [ -| FIELD +of_module_type: [ +| ":" module_type_inl +| check_module_types ] -fields: [ -| field fields -| field +is_module_type: [ +| ":=" module_type_inl LIST0 ext_module_type +| ] -fullyqualid: [ -| ident fields -| ident +is_module_expr: [ +| ":=" module_expr_inl LIST0 ext_module_expr +| ] -name: [ -| "_" -| ident +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| ] -reference: [ -| ident fields -| ident +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot ] -qualid: [ -| reference +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot ] -by_notation: [ -| ne_string OPT [ "%" IDENT ] +module_binder: [ +| "(" export_token LIST1 identref ":" module_type_inl ")" ] -smart_global: [ -| reference -| by_notation +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom ] -ne_string: [ -| STRING +module_expr_atom: [ +| qualid +| "(" module_expr ")" ] -ne_lstring: [ -| ne_string +with_declaration: [ +| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr +| "Module" fullyqualid ":=" qualid ] -dirpath: [ -| ident LIST0 field +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration ] -string: [ -| STRING +section_subset_expr: [ +| test_only_starredidentrefs LIST0 starredidentref +| ssexpr35 ] -lstring: [ -| string +starredidentref: [ +| identref +| identref "*" +| "Type" +| "Type" "*" ] -integer: [ -| bigint +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 ] -natural: [ -| bignat +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 ] -bigint: [ -| bignat -| test_minus_nat "-" bignat +ssexpr0: [ +| starredidentref +| "(" test_only_starredidentrefs LIST0 starredidentref ")" +| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" ] -bignat: [ -| NUMBER +args_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" ] -bar_cbrace: [ -| test_pipe_closedcurly "|" "}" +scope_delimiter: [ +| "%" IDENT ] -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" +argument_spec: [ +| OPT "!" name OPT scope_delimiter ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry +arg_specs: [ +| argument_spec +| "/" +| "&" +| "(" LIST1 argument_spec ")" OPT scope_delimiter +| "[" LIST1 argument_spec "]" OPT scope_delimiter +| "{" LIST1 argument_spec "}" OPT scope_delimiter ] -opt_hintbases: [ -| -| ":" LIST1 IDENT +implicits_alt: [ +| name +| "[" LIST1 name "]" +| "{" LIST1 name "}" ] -command: [ -| "Goal" lconstr -| "Proof" -| "Proof" "using" G_vernac.section_subset_expr -| "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 ":" term200 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 -| "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 -| "Set" setting_name option_setting -| "Unset" setting_name -| "Print" "Table" setting_name -| "Add" IDENT IDENT LIST1 table_value -| "Add" IDENT LIST1 table_value -| "Test" setting_name "for" LIST1 table_value -| "Test" setting_name -| "Remove" IDENT IDENT LIST1 table_value -| "Remove" IDENT LIST1 table_value -| "Write" "State" IDENT -| "Write" "State" ne_string -| "Restore" "State" IDENT -| "Restore" "State" ne_string -| "Reset" "Initial" -| "Reset" identref -| "Back" -| "Back" 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_fix_definition 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" LIST1 reference -| "Typeclasses" "Opaque" LIST1 reference -| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural -| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] -| "Proof" "using" G_vernac.section_subset_expr "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" natural "of" ident ":" lglob withtac -| "Obligation" natural "of" ident withtac -| "Obligation" natural ":" lglob withtac -| "Obligation" natural withtac -| "Next" "Obligation" "of" ident withtac -| "Next" "Obligation" withtac -| "Solve" "Obligation" natural "of" ident "with" tactic -| "Solve" "Obligation" natural "with" tactic -| "Solve" "Obligations" "of" ident "with" tactic -| "Solve" "Obligations" "of" ident -| "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" integer -| "Show" "Ltac" "Profile" string -| "Show" "Lia" "Profile" (* micromega plugin *) -| "Add" "Zify" "InjTyp" constr (* micromega plugin *) -| "Add" "Zify" "BinOp" constr (* micromega plugin *) -| "Add" "Zify" "UnOp" constr (* micromega plugin *) -| "Add" "Zify" "CstOp" constr (* micromega plugin *) -| "Add" "Zify" "BinRel" constr (* micromega plugin *) -| "Add" "Zify" "PropOp" constr (* micromega plugin *) -| "Add" "Zify" "PropBinOp" constr (* micromega plugin *) -| "Add" "Zify" "PropUOp" constr (* micromega plugin *) -| "Add" "Zify" "BinOpSpec" constr (* micromega plugin *) -| "Add" "Zify" "UnOpSpec" constr (* micromega plugin *) -| "Add" "Zify" "Saturate" constr (* micromega plugin *) -| "Show" "Zify" "InjTyp" (* micromega plugin *) -| "Show" "Zify" "BinOp" (* micromega plugin *) -| "Show" "Zify" "UnOp" (* micromega plugin *) -| "Show" "Zify" "CstOp" (* micromega plugin *) -| "Show" "Zify" "BinRel" (* micromega plugin *) -| "Show" "Zify" "UnOpSpec" (* micromega plugin *) -| "Show" "Zify" "BinOpSpec" (* micromega plugin *) -| "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *) -| "Print" "Rings" (* ring plugin *) -| "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) -| "Print" "Fields" (* ring plugin *) -| "Prenex" "Implicits" LIST1 global (* SSR plugin *) -| "Print" "Hint" "View" ssrviewpos (* SSR plugin *) -| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* SSR plugin *) -| "Search" ssr_search_arg ssr_modlocs (* SSR plugin *) -| "Number" "Notation" reference reference reference OPT number_options ":" ident -| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier -| "String" "Notation" reference reference reference OPT string_option ":" ident -| "Ltac2" ltac2_entry (* Ltac2 plugin *) -| "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) -| "Print" "Ltac2" reference (* Ltac2 plugin *) +instance_name: [ +| ident_decl binders +| ] -reference_or_constr: [ -| global -| constr +hint_info: [ +| "|" OPT natural OPT constr_pattern +| ] -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 +reserv_list: [ +| LIST1 reserv_tuple +| simple_reserv ] -constr_body: [ -| ":=" lconstr -| ":" lconstr ":=" lconstr +reserv_tuple: [ +| "(" simple_reserv ")" ] -mode: [ -| LIST1 [ "+" | "!" | "-" ] +simple_reserv: [ +| LIST1 identref ":" lconstr ] -vernac_control: [ -| "Time" vernac_control -| "Redirect" ne_string vernac_control -| "Timeout" natural vernac_control -| "Fail" vernac_control -| decorated_vernac +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global OPT univ_name_list "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" search_query search_queries "." ] -decorated_vernac: [ -| LIST0 quoted_attributes vernac +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" LIST0 smart_global +| "Typing" "Flags" +| "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" ] -quoted_attributes: [ -| "#[" attribute_list "]" +printunivs_subgraph: [ +| "Subgraph" "(" LIST0 reference ")" ] -attribute_list: [ -| LIST0 attribute SEP "," +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global ] -attribute: [ -| ident attr_value -| "using" attr_value +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global ] -attr_value: [ -| "=" string -| "=" IDENT -| "(" attribute_list ")" +option_setting: [ | +| integer +| STRING ] -legacy_attr: [ -| "Local" -| "Global" -| "Polymorphic" -| "Monomorphic" -| "Cumulative" -| "NonCumulative" -| "Private" -| "Program" +table_value: [ +| global +| STRING ] -vernac: [ -| LIST0 legacy_attr vernac_aux +setting_name: [ +| LIST1 IDENT ] -vernac_aux: [ -| gallina "." -| gallina_ext "." -| command "." -| syntax "." -| subprf -| command_entry +ne_in_or_out_modules: [ +| "inside" LIST1 global +| "outside" LIST1 global ] -noedit_mode: [ -| query_command +in_or_out_modules: [ +| ne_in_or_out_modules +| ] -subprf: [ -| BULLET -| "{" -| "}" +comment: [ +| constr +| STRING +| natural ] -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" ident_decl def_body -| finite_token LIST1 inductive_definition SEP "with" -| "Fixpoint" LIST1 fix_definition SEP "with" -| "Let" "Fixpoint" LIST1 fix_definition SEP "with" -| "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Scheme" LIST1 scheme SEP "with" -| "Combined" "Scheme" identref "from" LIST1 identref SEP "," -| "Register" global "as" qualid -| "Register" "Inline" global -| "Primitive" ident_decl OPT [ ":" lconstr ] ":=" register_token -| "Universe" LIST1 identref -| "Universes" LIST1 identref -| "Constraint" LIST1 univ_constraint SEP "," +positive_search_mark: [ +| "-" +| ] -register_token: [ -| test_hash_ident "#" IDENT +search_query: [ +| positive_search_mark search_item +| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]" ] -thm_token: [ -| "Theorem" -| "Lemma" -| "Fact" -| "Remark" -| "Corollary" -| "Proposition" -| "Property" +search_item: [ +| test_id_colon search_where ":" ne_string OPT scope_delimiter +| "is" ":" logical_kind +| ne_string OPT scope_delimiter +| test_id_colon search_where ":" constr_pattern +| constr_pattern ] -def_token: [ -| "Definition" -| "Example" -| "SubClass" +logical_kind: [ +| thm_token +| assumption_token +| "Context" +| extended_def_token +| "Primitive" ] -assumption_token: [ -| "Hypothesis" -| "Variable" -| "Axiom" -| "Parameter" -| "Conjecture" +extended_def_token: [ +| def_token +| "Coercion" +| "Instance" +| "Scheme" +| "Canonical" +| "Field" +| "Method" ] -assumptions_token: [ -| "Hypotheses" -| "Variables" -| "Axioms" -| "Parameters" -| "Conjectures" +search_where: [ +| "head" +| "hyp" +| "concl" +| "headhyp" +| "headconcl" ] -inline: [ -| "Inline" "(" natural ")" -| "Inline" +search_queries: [ +| ne_in_or_out_modules +| search_query search_queries | ] -univ_constraint: [ -| universe_name [ "<" | "=" | "<=" ] universe_name -] - -univ_decl: [ -| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +univ_name_list: [ +| "@{" LIST0 name "}" ] -variance: [ -| "+" -| "=" -| "*" +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 syntax_modifiers OPT [ ":" IDENT ] +| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring syntax_modifiers +| "Reserved" "Notation" ne_lstring syntax_modifiers ] -variance_identref: [ -| identref -| test_variance_ident variance identref +only_parsing: [ +| "(" "only" "parsing" ")" +| ] -cumul_univ_decl: [ -| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +level: [ +| "level" natural +| "next" "level" ] -ident_decl: [ -| identref OPT univ_decl +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "format" STRING OPT STRING +| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "at" level OPT binder_interp +| IDENT binder_interp +| IDENT explicit_subentry ] -cumul_ident_decl: [ -| identref OPT cumul_univ_decl +syntax_modifiers: [ +| "(" LIST1 syntax_modifier SEP "," ")" +| ] -finite_token: [ -| "Inductive" -| "CoInductive" -| "Variant" -| "Record" -| "Structure" -| "Class" +explicit_subentry: [ +| "ident" +| "name" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" at_level_opt OPT binder_interp +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT at_level_opt OPT binder_interp ] -def_body: [ -| binders ":=" reduce lconstr -| binders ":" lconstr ":=" reduce lconstr -| binders ":" lconstr +at_level_opt: [ +| "at" level +| ] -reduce: [ -| "Eval" red_expr "in" -| +binder_interp: [ +| "as" "ident" +| "as" "name" +| "as" "pattern" +| "as" "strict" "pattern" ] -decl_notation: [ -| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry ] -decl_sep: [ -| "and" +Constr.ident: [ +| Prim.ident ] -decl_notations: [ -| "where" LIST1 decl_notation SEP decl_sep -| +Prim.name: [ +| "_" ] -opt_constructors_or_fields: [ -| ":=" constructors_or_record -| +global: [ +| Prim.reference ] -inductive_definition: [ -| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +constr_pattern: [ +| constr ] -constructors_or_record: [ -| "|" LIST1 constructor SEP "|" -| identref constructor_type "|" LIST1 constructor SEP "|" -| identref constructor_type -| identref "{" record_fields "}" -| "{" record_fields "}" -| +cpattern: [ +| lconstr ] -opt_coercion: [ -| ">" -| +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" ] -fix_definition: [ -| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" ] -cofix_definition: [ -| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +universe_increment: [ +| "+" natural +| ] -scheme: [ -| scheme_kind -| identref ":=" scheme_kind +universe_name: [ +| global +| "Set" +| "Prop" ] -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 +universe_expr: [ +| universe_name universe_increment ] -record_field: [ -| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr ] -record_fields: [ -| record_field ";" record_fields -| record_field -| +lconstr: [ +| term200 ] -field_body: [ -| binders of_type lconstr -| binders of_type lconstr ":=" lconstr -| binders ":=" lconstr +constr: [ +| term8 +| "@" global univ_annot ] -record_binder: [ -| name -| name field_body +term200: [ +| binder_constr +| term100 ] -assum_list: [ -| LIST1 assum_coe -| assumpt +term100: [ +| term99 "<:" term200 +| term99 "<<:" term200 +| term99 ":" term200 +| term99 ":>" +| term99 ] -assum_coe: [ -| "(" assumpt ")" +term99: [ +| term90 ] -assumpt: [ -| LIST1 ident_decl of_type lconstr +term90: [ +| term10 ] -constructor_type: [ -| binders [ of_type lconstr | ] +term10: [ +| term9 LIST1 arg +| "@" global univ_annot LIST0 term9 +| "@" pattern_ident LIST1 identref +| term9 ] -constructor: [ -| identref constructor_type +term9: [ +| ".." term0 ".." +| term8 ] -of_type: [ -| ":>" -| ":" ">" -| ":" +term8: [ +| term1 ] -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 -| "End" identref -| "Collection" identref ":=" section_subset_expr -| "Require" export_token LIST1 global -| "From" global "Require" export_token LIST1 global -| "Import" LIST1 filtered_import -| "Export" LIST1 filtered_import -| "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 ":" term200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] -| "Existing" "Instance" global hint_info -| "Existing" "Instances" LIST1 global OPT [ "|" natural ] -| "Existing" "Class" global -| "Arguments" smart_global LIST0 arg_specs OPT [ "," LIST1 [ LIST0 implicits_alt ] SEP "," ] OPT [ ":" LIST1 args_modifier SEP "," ] -| "Implicit" "Type" reserv_list -| "Implicit" "Types" reserv_list -| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] -| "Export" "Set" setting_name option_setting -| "Export" "Unset" setting_name -| "Import" "Prenex" "Implicits" (* SSR plugin *) +term1: [ +| term0 ".(" global LIST0 arg ")" +| term0 ".(" "@" global LIST0 ( term9 ) ")" +| term0 "%" IDENT +| term0 ] -filtered_import: [ -| global -| global "(" LIST1 one_import_filter_name SEP "," ")" +term0: [ +| atomic_constr +| term_match +| "(" term200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" term200 "}" +| test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot +| "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" ] -one_import_filter_name: [ -| global OPT [ "(" ".." ")" ] +array_elems: [ +| LIST0 lconstr SEP ";" ] -export_token: [ -| "Import" -| "Export" +record_declaration: [ +| fields_def +] + +fields_def: [ +| field_def ";" fields_def +| field_def | ] -ext_module_type: [ -| "<+" module_type_inl +field_def: [ +| global binders ":=" lconstr ] -ext_module_expr: [ -| "<+" module_expr_inl +binder_constr: [ +| "forall" open_binders "," term200 +| "fun" open_binders "=>" term200 +| "let" name binders let_type_cstr ":=" term200 "in" term200 +| "let" "fix" fix_decl "in" term200 +| "let" "cofix" cofix_body "in" term200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 "in" term200 +| "let" "'" pattern200 ":=" term200 case_type "in" term200 +| "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200 +| "if" term200 as_return_type "then" term200 "else" term200 +| "fix" fix_decls +| "cofix" cofix_decls +| "if" term200 "is" ssr_dthen ssr_else (* SSR plugin *) +| "if" term200 "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 *) ] -check_module_type: [ -| "<:" module_type_inl +arg: [ +| test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| term9 ] -check_module_types: [ -| LIST0 check_module_type +atomic_constr: [ +| global univ_annot +| sort +| NUMBER +| string +| "_" +| "?" "[" identref "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance ] -of_module_type: [ -| ":" module_type_inl -| check_module_types +inst: [ +| identref ":=" lconstr ] -is_module_type: [ -| ":=" module_type_inl LIST0 ext_module_type +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" | ] -is_module_expr: [ -| ":=" module_expr_inl LIST0 ext_module_expr +univ_annot: [ +| "@{" LIST0 universe_level "}" | ] -functor_app_annot: [ -| "[" "inline" "at" "level" natural "]" -| "[" "no" "inline" "]" -| +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global ] -module_expr_inl: [ -| "!" module_expr -| module_expr functor_app_annot +fix_decls: [ +| fix_decl +| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref ] -module_type_inl: [ -| "!" module_type -| module_type functor_app_annot +cofix_decls: [ +| cofix_body +| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref ] -module_binder: [ -| "(" export_token LIST1 identref ":" module_type_inl ")" +fix_decl: [ +| identref binders_fixannot type_cstr ":=" term200 ] -module_expr: [ -| module_expr_atom -| module_expr module_expr_atom +cofix_body: [ +| identref binders type_cstr ":=" term200 ] -module_expr_atom: [ -| qualid -| "(" module_expr ")" +term_match: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" ] -with_declaration: [ -| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr -| "Module" fullyqualid ":=" qualid +case_item: [ +| term100 OPT [ "as" name ] OPT [ "in" pattern200 ] ] -module_type: [ -| qualid -| "(" module_type ")" -| module_type module_expr_atom -| module_type "with" with_declaration +case_type: [ +| "return" term100 ] -section_subset_expr: [ -| test_only_starredidentrefs LIST0 starredidentref -| ssexpr35 +as_return_type: [ +| OPT [ OPT [ "as" name ] case_type ] ] -starredidentref: [ -| identref -| identref "*" -| "Type" -| "Type" "*" +branches: [ +| OPT "|" LIST0 eqn SEP "|" ] -ssexpr35: [ -| "-" ssexpr50 -| ssexpr50 +mult_pattern: [ +| LIST1 pattern200 SEP "," ] -ssexpr50: [ -| ssexpr0 "-" ssexpr0 -| ssexpr0 "+" ssexpr0 -| ssexpr0 +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr ] -ssexpr0: [ -| starredidentref -| "(" test_only_starredidentrefs LIST0 starredidentref ")" -| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*" -| "(" ssexpr35 ")" -| "(" ssexpr35 ")" "*" +record_pattern: [ +| global ":=" pattern200 ] -args_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" +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern +| ] -scope_delimiter: [ -| "%" IDENT +pattern200: [ +| pattern100 ] -argument_spec: [ -| OPT "!" name OPT scope_delimiter +pattern100: [ +| pattern99 ":" term200 +| pattern99 ] -arg_specs: [ -| argument_spec -| "/" -| "&" -| "(" LIST1 argument_spec ")" OPT scope_delimiter -| "[" LIST1 argument_spec "]" OPT scope_delimiter -| "{" LIST1 argument_spec "}" OPT scope_delimiter +pattern99: [ +| pattern90 ] -implicits_alt: [ -| name -| "[" LIST1 name "]" -| "{" LIST1 name "}" +pattern90: [ +| pattern10 ] -instance_name: [ -| ident_decl binders -| +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 ] -hint_info: [ -| "|" OPT natural OPT constr_pattern +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMBER +| string +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +] + +binders_fixannot: [ +| ensure_fixannot fixannot +| binder binders_fixannot | ] -reserv_list: [ -| LIST1 reserv_tuple -| simple_reserv +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 "}" +| "[" name "]" +| "[" name LIST1 name ":" lconstr "]" +| "[" name ":" lconstr "]" +| "[" name LIST1 name "]" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" +| "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) ] -reserv_tuple: [ -| "(" simple_reserv ")" +one_open_binder: [ +| name +| name ":" lconstr +| one_closed_binder ] -simple_reserv: [ -| LIST1 identref ":" lconstr +one_closed_binder: [ +| "(" name ":" lconstr ")" +| "{" name "}" +| "{" name ":" lconstr "}" +| "[" name "]" +| "[" name ":" lconstr "]" +| "'" pattern0 ] -query_command: [ -| "Eval" red_expr "in" lconstr "." -| "Compute" lconstr "." -| "Check" lconstr "." -| "About" smart_global OPT univ_name_list "." -| "SearchPattern" constr_pattern in_or_out_modules "." -| "SearchRewrite" constr_pattern in_or_out_modules "." -| "Search" search_query search_queries "." +typeclass_constraint: [ +| "!" term200 +| "{" name "}" ":" [ "!" | ] term200 +| test_name_colon name ":" [ "!" | ] term200 +| term200 ] -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" LIST0 smart_global -| "Typing" "Flags" -| "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" +type_cstr: [ +| ":" lconstr +| ] -printunivs_subgraph: [ -| "Subgraph" "(" LIST0 reference ")" +let_type_cstr: [ +| OPT [ ":" lconstr ] ] -class_rawexpr: [ -| "Funclass" -| "Sortclass" -| smart_global +preident: [ +| IDENT ] -locatable: [ -| smart_global -| "Term" smart_global -| "File" ne_string -| "Library" global -| "Module" global +ident: [ +| IDENT ] -option_setting: [ -| -| integer -| STRING +pattern_ident: [ +| LEFTQMARK ident ] -table_value: [ -| global -| STRING +identref: [ +| ident ] -setting_name: [ -| LIST1 IDENT +hyp: [ +| identref ] -ne_in_or_out_modules: [ -| "inside" LIST1 global -| "outside" LIST1 global +field: [ +| FIELD ] -in_or_out_modules: [ -| ne_in_or_out_modules -| +fields: [ +| field fields +| field ] -comment: [ -| constr -| STRING -| natural +fullyqualid: [ +| ident fields +| ident ] -positive_search_mark: [ -| "-" -| +name: [ +| "_" +| ident ] -search_query: [ -| positive_search_mark search_item -| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]" +reference: [ +| ident fields +| ident ] -search_item: [ -| test_id_colon search_where ":" ne_string OPT scope_delimiter -| "is" ":" logical_kind -| ne_string OPT scope_delimiter -| test_id_colon search_where ":" constr_pattern -| constr_pattern +qualid: [ +| reference ] -logical_kind: [ -| thm_token -| assumption_token -| "Context" -| extended_def_token -| "Primitive" +by_notation: [ +| ne_string OPT [ "%" IDENT ] ] -extended_def_token: [ -| def_token -| "Coercion" -| "Instance" -| "Scheme" -| "Canonical" -| "Field" -| "Method" +smart_global: [ +| reference +| by_notation ] -search_where: [ -| "head" -| "hyp" -| "concl" -| "headhyp" -| "headconcl" +ne_string: [ +| STRING ] -search_queries: [ -| ne_in_or_out_modules -| search_query search_queries -| +ne_lstring: [ +| ne_string ] -univ_name_list: [ -| "@{" LIST0 name "}" +dirpath: [ +| ident LIST0 field ] -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 syntax_modifiers OPT [ ":" IDENT ] -| "Notation" identref LIST0 ident ":=" constr only_parsing -| "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] -| "Format" "Notation" STRING STRING STRING -| "Reserved" "Infix" ne_lstring syntax_modifiers -| "Reserved" "Notation" ne_lstring syntax_modifiers +string: [ +| STRING ] -only_parsing: [ -| "(" "only" "parsing" ")" -| +lstring: [ +| string ] -level: [ -| "level" natural -| "next" "level" +integer: [ +| bigint ] -syntax_modifier: [ -| "at" "level" natural -| "in" "custom" IDENT -| "in" "custom" IDENT; "at" "level" natural -| "left" "associativity" -| "right" "associativity" -| "no" "associativity" -| "only" "printing" -| "only" "parsing" -| "format" STRING OPT STRING -| IDENT; "," LIST1 IDENT SEP "," "at" level -| IDENT; "at" level OPT binder_interp -| IDENT binder_interp -| IDENT explicit_subentry +natural: [ +| bignat ] -syntax_modifiers: [ -| "(" LIST1 syntax_modifier SEP "," ")" -| +bigint: [ +| bignat +| test_minus_nat "-" bignat ] -explicit_subentry: [ -| "ident" -| "name" -| "global" -| "bigint" -| "binder" -| "constr" -| "constr" at_level_opt OPT binder_interp -| "pattern" -| "pattern" "at" "level" natural -| "strict" "pattern" -| "strict" "pattern" "at" "level" natural -| "closed" "binder" -| "custom" IDENT at_level_opt OPT binder_interp +bignat: [ +| NUMBER ] -at_level_opt: [ -| "at" level -| +bar_cbrace: [ +| test_pipe_closedcurly "|" "}" ] -binder_interp: [ -| "as" "ident" -| "as" "name" -| "as" "pattern" -| "as" "strict" "pattern" +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" ] simple_tactic: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a34e96ac16..5674d28139 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -337,7 +337,7 @@ NOTINRSTS: [ | q_destruction_arg | q_with_bindings | q_bindings -| q_strategy_flag +| q_reductions | q_reference | q_clause | q_occurrences @@ -550,9 +550,9 @@ term_generalizing: [ ] term_cast: [ +| term10 ":" type | term10 "<:" type | term10 "<<:" type -| term10 ":" type | term10 ":>" ] @@ -627,38 +627,38 @@ reduce: [ ] red_expr: [ -| "red" -| "hnf" -| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] -| "cbv" OPT strategy_flag -| "cbn" OPT strategy_flag -| "lazy" OPT strategy_flag -| "compute" OPT delta_flag +| "lazy" OPT reductions +| "cbv" OPT reductions +| "compute" OPT delta_reductions | "vm_compute" OPT [ reference_occs | pattern_occs ] | "native_compute" OPT [ reference_occs | pattern_occs ] +| "red" +| "hnf" +| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] +| "cbn" OPT reductions | "unfold" LIST1 reference_occs SEP "," | "fold" LIST1 one_term | "pattern" LIST1 pattern_occs SEP "," | ident ] -delta_flag: [ -| OPT "-" "[" LIST1 reference "]" -] - -strategy_flag: [ -| LIST1 red_flag -| delta_flag +reductions: [ +| LIST1 reduction +| delta_reductions ] -red_flag: [ +reduction: [ | "beta" -| "iota" +| "delta" OPT delta_reductions | "match" | "fix" | "cofix" +| "iota" | "zeta" -| "delta" OPT delta_flag +] + +delta_reductions: [ +| OPT "-" "[" LIST1 reference "]" ] reference_occs: [ @@ -1242,6 +1242,10 @@ occurrences: [ | "in" goal_occurrences ] +simple_occurrences: [ +| occurrences +] + occs_nums: [ | OPT "-" LIST1 nat_or_var ] @@ -1741,7 +1745,7 @@ simple_tactic: [ | "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases | "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases -| "autounfold" OPT hintbases OPT occurrences +| "autounfold" OPT hintbases OPT simple_occurrences | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident ) @@ -1811,17 +1815,17 @@ simple_tactic: [ | "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) | "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident ) -| "red" OPT occurrences -| "hnf" OPT occurrences -| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] OPT occurrences -| "cbv" OPT strategy_flag OPT occurrences -| "cbn" OPT strategy_flag OPT occurrences -| "lazy" OPT strategy_flag OPT occurrences -| "compute" OPT delta_flag OPT occurrences +| "red" simple_occurrences +| "hnf" simple_occurrences +| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences +| "cbv" OPT reductions simple_occurrences +| "cbn" OPT reductions simple_occurrences +| "lazy" OPT reductions simple_occurrences +| "compute" OPT delta_reductions simple_occurrences | "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences | "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences | "unfold" LIST1 reference_occs SEP "," OPT occurrences -| "fold" LIST1 one_term OPT occurrences +| "fold" LIST1 one_term simple_occurrences | "pattern" LIST1 pattern_occs SEP "," OPT occurrences | "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences | "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences @@ -2139,13 +2143,13 @@ ltac2_goal_tactics: [ | LIST0 ( OPT ltac2_expr ) SEP "|" (* Ltac2 plugin *) ] -q_strategy_flag: [ -| ltac2_strategy_flag (* Ltac2 plugin *) +q_reductions: [ +| ltac2_reductions (* Ltac2 plugin *) ] -ltac2_strategy_flag: [ +ltac2_reductions: [ | LIST1 ltac2_red_flag (* Ltac2 plugin *) -| OPT ltac2_delta_flag (* Ltac2 plugin *) +| OPT ltac2_delta_reductions (* Ltac2 plugin *) ] ltac2_red_flag: [ @@ -2155,10 +2159,10 @@ ltac2_red_flag: [ | "fix" (* Ltac2 plugin *) | "cofix" (* Ltac2 plugin *) | "zeta" (* Ltac2 plugin *) -| "delta" OPT ltac2_delta_flag (* Ltac2 plugin *) +| "delta" OPT ltac2_delta_reductions (* Ltac2 plugin *) ] -ltac2_delta_flag: [ +ltac2_delta_reductions: [ | OPT "-" "[" LIST1 refglobal "]" ] -- cgit v1.2.3