From aba594ca194390bb00f8ef60ef8a5eef6694fc07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 10 Mar 2021 12:17:32 +0100
Subject: Regenerate the Ltac2 syntax for documentation.

---
 doc/tools/docgram/common.edit_mlg |    1 +
 doc/tools/docgram/fullGrammar     | 2125 +++++++++++++++++++------------------
 doc/tools/docgram/orderedGrammar  |    6 +-
 3 files changed, 1069 insertions(+), 1063 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 24ecc65e9b..fd1c3c0260 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2730,6 +2730,7 @@ SPLICE: [
 | variance_identref
 | rewriter
 | conversion
+| type_cast
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index be1b9d80fb..ab1a9d4c75 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
 
-opt_hintbases: [
-|
-| ":" LIST1 IDENT
+Constr.ident: [
+| Prim.ident
 ]
 
-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 *)
+Prim.name: [
+| "_"
 ]
 
-reference_or_constr: [
-| global
-| constr
+global: [
+| Prim.reference
 ]
 
-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_pattern: [
+| constr
 ]
 
-constr_body: [
-| ":=" lconstr
-| ":" lconstr ":=" lconstr
+cpattern: [
+| lconstr
 ]
 
-mode: [
-| LIST1 [ "+" | "!" | "-" ]
+sort: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
+| "Type" "@{" "_" "}"
+| "Type" "@{" universe "}"
 ]
 
-vernac_control: [
-| "Time" vernac_control
-| "Redirect" ne_string vernac_control
-| "Timeout" natural vernac_control
-| "Fail" vernac_control
-| decorated_vernac
+sort_family: [
+| "Set"
+| "Prop"
+| "SProp"
+| "Type"
 ]
 
-decorated_vernac: [
-| LIST0 quoted_attributes vernac
+universe_increment: [
+| "+" natural
+|
 ]
 
-quoted_attributes: [
-| "#[" attribute_list "]"
+universe_name: [
+| global
+| "Set"
+| "Prop"
 ]
 
-attribute_list: [
-| LIST0 attribute SEP ","
+universe_expr: [
+| universe_name universe_increment
 ]
 
-attribute: [
-| ident attr_value
-| "using" attr_value
+universe: [
+| "max" "(" LIST1 universe_expr SEP "," ")"
+| universe_expr
 ]
 
-attr_value: [
-| "=" string
-| "=" IDENT
-| "(" attribute_list ")"
-|
+lconstr: [
+| term200
 ]
 
-legacy_attr: [
-| "Local"
-| "Global"
-| "Polymorphic"
-| "Monomorphic"
-| "Cumulative"
-| "NonCumulative"
-| "Private"
-| "Program"
+constr: [
+| term8
+| "@" global univ_annot
 ]
 
-vernac: [
-| LIST0 legacy_attr vernac_aux
+term200: [
+| binder_constr
+| term100
 ]
 
-vernac_aux: [
-| gallina "."
-| gallina_ext "."
-| command "."
-| syntax "."
-| subprf
-| command_entry
+term100: [
+| term99 "<:" term200
+| term99 "<<:" term200
+| term99 ":" term200
+| term99 ":>"
+| term99
 ]
 
-noedit_mode: [
-| query_command
+term99: [
+| term90
 ]
 
-subprf: [
-| BULLET
-| "{"
-| "}"
+term90: [
+| term10
 ]
 
-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 ","
+term10: [
+| term9 LIST1 arg
+| "@" global univ_annot LIST0 term9
+| "@" pattern_ident LIST1 identref
+| term9
 ]
 
-register_token: [
-| test_hash_ident "#" IDENT
+term9: [
+| ".." term0 ".."
+| term8
 ]
 
-thm_token: [
-| "Theorem"
-| "Lemma"
-| "Fact"
-| "Remark"
-| "Corollary"
-| "Proposition"
-| "Property"
+term8: [
+| term1
 ]
 
-def_token: [
-| "Definition"
-| "Example"
-| "SubClass"
+term1: [
+| term0 ".(" global LIST0 arg ")"
+| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 "%" IDENT
+| term0
 ]
 
-assumption_token: [
-| "Hypothesis"
-| "Variable"
-| "Axiom"
-| "Parameter"
-| "Conjecture"
+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 ")"
 ]
 
-assumptions_token: [
-| "Hypotheses"
-| "Variables"
-| "Axioms"
-| "Parameters"
-| "Conjectures"
+array_elems: [
+| LIST0 lconstr SEP ";"
 ]
 
-inline: [
-| "Inline" "(" natural ")"
-| "Inline"
-|
+record_declaration: [
+| fields_def
 ]
 
-univ_constraint: [
-| universe_name [ "<" | "=" | "<=" ] universe_name
+fields_def: [
+| field_def ";" fields_def
+| field_def
+|
 ]
 
-univ_decl: [
-| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+field_def: [
+| global binders ":=" lconstr
 ]
 
-variance: [
-| "+"
-| "="
-| "*"
+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 *)
 ]
 
-variance_identref: [
-| identref
-| test_variance_ident variance identref
+arg: [
+| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
+| term9
 ]
 
-cumul_univ_decl: [
-| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
+atomic_constr: [
+| global univ_annot
+| sort
+| NUMBER
+| string
+| "_"
+| "?" "[" identref "]"
+| "?" "[" pattern_ident "]"
+| pattern_ident evar_instance
 ]
 
-ident_decl: [
-| identref OPT univ_decl
+inst: [
+| identref ":=" lconstr
 ]
 
-cumul_ident_decl: [
-| identref OPT cumul_univ_decl
+evar_instance: [
+| "@{" LIST1 inst SEP ";" "}"
+|
 ]
 
-finite_token: [
-| "Inductive"
-| "CoInductive"
-| "Variant"
-| "Record"
-| "Structure"
-| "Class"
+univ_annot: [
+| "@{" LIST0 universe_level "}"
+|
 ]
 
-def_body: [
-| binders ":=" reduce lconstr
-| binders ":" lconstr ":=" reduce lconstr
-| binders ":" lconstr
+universe_level: [
+| "Set"
+| "Prop"
+| "Type"
+| "_"
+| global
 ]
 
-reduce: [
-| "Eval" red_expr "in"
-|
+fix_decls: [
+| fix_decl
+| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
 ]
 
-decl_notation: [
-| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
+cofix_decls: [
+| cofix_body
+| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
 ]
 
-decl_sep: [
-| "and"
+fix_decl: [
+| identref binders_fixannot type_cstr ":=" term200
 ]
 
-decl_notations: [
-| "where" LIST1 decl_notation SEP decl_sep
-|
+cofix_body: [
+| identref binders type_cstr ":=" term200
 ]
 
-opt_constructors_or_fields: [
-| ":=" constructors_or_record
-|
+term_match: [
+| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
 ]
 
-inductive_definition: [
-| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
+case_item: [
+| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
 ]
 
-constructors_or_record: [
-| "|" LIST1 constructor SEP "|"
-| identref constructor_type "|" LIST1 constructor SEP "|"
-| identref constructor_type
-| identref "{" record_fields "}"
-| "{" record_fields "}"
-|
+case_type: [
+| "return" term100
 ]
 
-opt_coercion: [
-| ">"
-|
+as_return_type: [
+| OPT [ OPT [ "as" name ] case_type ]
 ]
 
-fix_definition: [
-| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
+branches: [
+| OPT "|" LIST0 eqn SEP "|"
 ]
 
-cofix_definition: [
-| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
+mult_pattern: [
+| LIST1 pattern200 SEP ","
 ]
 
-scheme: [
-| scheme_kind
-| identref ":=" scheme_kind
+eqn: [
+| LIST1 mult_pattern SEP "|" "=>" lconstr
 ]
 
-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_pattern: [
+| global ":=" pattern200
 ]
 
-record_field: [
-| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations
+record_patterns: [
+| record_pattern ";" record_patterns
+| record_pattern
+|
 ]
 
-record_fields: [
-| record_field ";" record_fields
-| record_field
-|
+pattern200: [
+| pattern100
 ]
 
-field_body: [
-| binders of_type lconstr
-| binders of_type lconstr ":=" lconstr
-| binders ":=" lconstr
+pattern100: [
+| pattern99 ":" term200
+| pattern99
 ]
 
-record_binder: [
-| name
-| name field_body
+pattern99: [
+| pattern90
 ]
 
-assum_list: [
-| LIST1 assum_coe
-| assumpt
+pattern90: [
+| pattern10
 ]
 
-assum_coe: [
-| "(" assumpt ")"
+pattern10: [
+| pattern1 "as" name
+| pattern1 LIST1 pattern1
+| "@" Prim.reference LIST0 pattern1
+| pattern1
 ]
 
-assumpt: [
-| LIST1 ident_decl of_type lconstr
+pattern1: [
+| pattern0 "%" IDENT
+| pattern0
 ]
 
-constructor_type: [
-| binders [ of_type lconstr | ]
+pattern0: [
+| Prim.reference
+| "{|" record_patterns bar_cbrace
+| "_"
+| "(" pattern200 ")"
+| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
+| NUMBER
+| string
 ]
 
-constructor: [
-| identref constructor_type
+fixannot: [
+| "{" "struct" identref "}"
+| "{" "wf" constr identref "}"
+| "{" "measure" constr OPT identref OPT constr "}"
 ]
 
-of_type: [
-| ":>"
-| ":" ">"
-| ":"
+binders_fixannot: [
+| ensure_fixannot fixannot
+| binder binders_fixannot
+|
 ]
 
-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 *)
+open_binders: [
+| name LIST0 name ":" lconstr
+| name LIST0 name binders
+| name ".." name
+| closed_binder binders
 ]
 
-filtered_import: [
-| global
-| global "(" LIST1 one_import_filter_name SEP "," ")"
+binders: [
+| LIST0 binder
+| Pcoq.Constr.binders
 ]
 
-one_import_filter_name: [
-| global OPT [ "(" ".." ")" ]
+binder: [
+| name
+| closed_binder
 ]
 
-export_token: [
-| "Import"
-| "Export"
-|
+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 *)
 ]
 
-ext_module_type: [
-| "<+" module_type_inl
+one_open_binder: [
+| name
+| name ":" lconstr
+| one_closed_binder
 ]
 
-ext_module_expr: [
-| "<+" module_expr_inl
+one_closed_binder: [
+| "(" name ":" lconstr ")"
+| "{" name "}"
+| "{" name ":" lconstr "}"
+| "[" name "]"
+| "[" name ":" lconstr "]"
+| "'" pattern0
 ]
 
-check_module_type: [
-| "<:" module_type_inl
+typeclass_constraint: [
+| "!" term200
+| "{" name "}" ":" [ "!" | ] term200
+| test_name_colon name ":" [ "!" | ] term200
+| term200
 ]
 
-check_module_types: [
-| LIST0 check_module_type
+type_cstr: [
+| ":" lconstr
+|
 ]
 
-of_module_type: [
-| ":" module_type_inl
-| check_module_types
+let_type_cstr: [
+| OPT [ ":" lconstr ]
 ]
 
-is_module_type: [
-| ":=" module_type_inl LIST0 ext_module_type
-|
+preident: [
+| IDENT
 ]
 
-is_module_expr: [
-| ":=" module_expr_inl LIST0 ext_module_expr
-|
+ident: [
+| IDENT
 ]
 
-functor_app_annot: [
-| "[" "inline" "at" "level" natural "]"
-| "[" "no" "inline" "]"
-|
+pattern_ident: [
+| LEFTQMARK ident
 ]
 
-module_expr_inl: [
-| "!" module_expr
-| module_expr functor_app_annot
+identref: [
+| ident
 ]
 
-module_type_inl: [
-| "!" module_type
-| module_type functor_app_annot
+hyp: [
+| identref
 ]
 
-module_binder: [
-| "(" export_token LIST1 identref ":" module_type_inl ")"
+field: [
+| FIELD
 ]
 
-module_expr: [
-| module_expr_atom
-| module_expr module_expr_atom
+fields: [
+| field fields
+| field
 ]
 
-module_expr_atom: [
-| qualid
-| "(" module_expr ")"
+fullyqualid: [
+| ident fields
+| ident
 ]
 
-with_declaration: [
-| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
-| "Module" fullyqualid ":=" qualid
+name: [
+| "_"
+| ident
 ]
 
-module_type: [
-| qualid
-| "(" module_type ")"
-| module_type module_expr_atom
-| module_type "with" with_declaration
+reference: [
+| ident fields
+| ident
 ]
 
-section_subset_expr: [
-| test_only_starredidentrefs LIST0 starredidentref
-| ssexpr35
+qualid: [
+| reference
 ]
 
-starredidentref: [
-| identref
-| identref "*"
-| "Type"
-| "Type" "*"
+by_notation: [
+| ne_string OPT [ "%" IDENT ]
 ]
 
-ssexpr35: [
-| "-" ssexpr50
-| ssexpr50
+smart_global: [
+| reference
+| by_notation
 ]
 
-ssexpr50: [
-| ssexpr0 "-" ssexpr0
-| ssexpr0 "+" ssexpr0
-| ssexpr0
+ne_string: [
+| STRING
 ]
 
-ssexpr0: [
-| starredidentref
-| "(" test_only_starredidentrefs LIST0 starredidentref ")"
-| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*"
-| "(" ssexpr35 ")"
-| "(" ssexpr35 ")" "*"
+ne_lstring: [
+| ne_string
 ]
 
-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"
+dirpath: [
+| ident LIST0 field
 ]
 
-scope_delimiter: [
-| "%" IDENT
+string: [
+| STRING
 ]
 
-argument_spec: [
-| OPT "!" name OPT scope_delimiter
+lstring: [
+| string
 ]
 
-arg_specs: [
-| argument_spec
-| "/"
-| "&"
-| "(" LIST1 argument_spec ")" OPT scope_delimiter
-| "[" LIST1 argument_spec "]" OPT scope_delimiter
-| "{" LIST1 argument_spec "}" OPT scope_delimiter
+integer: [
+| bigint
 ]
 
-implicits_alt: [
-| name
-| "[" LIST1 name "]"
-| "{" LIST1 name "}"
+natural: [
+| bignat
 ]
 
-instance_name: [
-| ident_decl binders
-|
+bigint: [
+| bignat
+| test_minus_nat "-" bignat
 ]
 
-hint_info: [
-| "|" OPT natural OPT constr_pattern
-|
+bignat: [
+| NUMBER
 ]
 
-reserv_list: [
-| LIST1 reserv_tuple
-| simple_reserv
+bar_cbrace: [
+| test_pipe_closedcurly "|" "}"
 ]
 
-reserv_tuple: [
-| "(" simple_reserv ")"
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
 ]
 
-simple_reserv: [
-| LIST1 identref ":" lconstr
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
 ]
 
-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 "."
+opt_hintbases: [
+|
+| ":" LIST1 IDENT
 ]
 
-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"
+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 *)
 ]
 
-printunivs_subgraph: [
-| "Subgraph" "(" LIST0 reference ")"
+reference_or_constr: [
+| global
+| constr
 ]
 
-class_rawexpr: [
-| "Funclass"
-| "Sortclass"
-| smart_global
+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
 ]
 
-locatable: [
-| smart_global
-| "Term" smart_global
-| "File" ne_string
-| "Library" global
-| "Module" global
+constr_body: [
+| ":=" lconstr
+| ":" lconstr ":=" lconstr
 ]
 
-option_setting: [
-|
-| integer
-| STRING
+mode: [
+| LIST1 [ "+" | "!" | "-" ]
 ]
 
-table_value: [
-| global
-| STRING
+vernac_control: [
+| "Time" vernac_control
+| "Redirect" ne_string vernac_control
+| "Timeout" natural vernac_control
+| "Fail" vernac_control
+| decorated_vernac
 ]
 
-setting_name: [
-| LIST1 IDENT
+decorated_vernac: [
+| LIST0 quoted_attributes vernac
 ]
 
-ne_in_or_out_modules: [
-| "inside" LIST1 global
-| "outside" LIST1 global
+quoted_attributes: [
+| "#[" attribute_list "]"
 ]
 
-in_or_out_modules: [
-| ne_in_or_out_modules
-|
+attribute_list: [
+| LIST0 attribute SEP ","
 ]
 
-comment: [
-| constr
-| STRING
-| natural
+attribute: [
+| ident attr_value
+| "using" attr_value
 ]
 
-positive_search_mark: [
-| "-"
+attr_value: [
+| "=" string
+| "=" IDENT
+| "(" attribute_list ")"
 |
 ]
 
-search_query: [
-| positive_search_mark search_item
-| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
-]
-
-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
-]
-
-logical_kind: [
-| thm_token
-| assumption_token
-| "Context"
-| extended_def_token
-| "Primitive"
+legacy_attr: [
+| "Local"
+| "Global"
+| "Polymorphic"
+| "Monomorphic"
+| "Cumulative"
+| "NonCumulative"
+| "Private"
+| "Program"
 ]
 
-extended_def_token: [
-| def_token
-| "Coercion"
-| "Instance"
-| "Scheme"
-| "Canonical"
-| "Field"
-| "Method"
+vernac: [
+| LIST0 legacy_attr vernac_aux
 ]
 
-search_where: [
-| "head"
-| "hyp"
-| "concl"
-| "headhyp"
-| "headconcl"
+vernac_aux: [
+| gallina "."
+| gallina_ext "."
+| command "."
+| syntax "."
+| subprf
+| command_entry
 ]
 
-search_queries: [
-| ne_in_or_out_modules
-| search_query search_queries
-|
+noedit_mode: [
+| query_command
 ]
 
-univ_name_list: [
-| "@{" LIST0 name "}"
+subprf: [
+| BULLET
+| "{"
+| "}"
 ]
 
-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
+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 ","
 ]
 
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
+register_token: [
+| test_hash_ident "#" IDENT
 ]
 
-level: [
-| "level" natural
-| "next" "level"
+thm_token: [
+| "Theorem"
+| "Lemma"
+| "Fact"
+| "Remark"
+| "Corollary"
+| "Proposition"
+| "Property"
 ]
-
-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
+
+def_token: [
+| "Definition"
+| "Example"
+| "SubClass"
 ]
 
-syntax_modifiers: [
-| "(" LIST1 syntax_modifier SEP "," ")"
-|
+assumption_token: [
+| "Hypothesis"
+| "Variable"
+| "Axiom"
+| "Parameter"
+| "Conjecture"
 ]
 
-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
+assumptions_token: [
+| "Hypotheses"
+| "Variables"
+| "Axioms"
+| "Parameters"
+| "Conjectures"
 ]
 
-at_level_opt: [
-| "at" level
+inline: [
+| "Inline" "(" natural ")"
+| "Inline"
 |
 ]
 
-binder_interp: [
-| "as" "ident"
-| "as" "name"
-| "as" "pattern"
-| "as" "strict" "pattern"
+univ_constraint: [
+| universe_name [ "<" | "=" | "<=" ] universe_name
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
+univ_decl: [
+| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
 ]
 
-Constr.ident: [
-| Prim.ident
+variance: [
+| "+"
+| "="
+| "*"
 ]
 
-Prim.name: [
-| "_"
+variance_identref: [
+| identref
+| test_variance_ident variance identref
 ]
 
-global: [
-| Prim.reference
+cumul_univ_decl: [
+| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ]
 ]
 
-constr_pattern: [
-| constr
+ident_decl: [
+| identref OPT univ_decl
 ]
 
-cpattern: [
-| lconstr
+cumul_ident_decl: [
+| identref OPT cumul_univ_decl
 ]
 
-sort: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
-| "Type" "@{" "_" "}"
-| "Type" "@{" universe "}"
+finite_token: [
+| "Inductive"
+| "CoInductive"
+| "Variant"
+| "Record"
+| "Structure"
+| "Class"
 ]
 
-sort_family: [
-| "Set"
-| "Prop"
-| "SProp"
-| "Type"
+def_body: [
+| binders ":=" reduce lconstr
+| binders ":" lconstr ":=" reduce lconstr
+| binders ":" lconstr
 ]
 
-universe_increment: [
-| "+" natural
+reduce: [
+| "Eval" red_expr "in"
 |
 ]
 
-universe_name: [
-| global
-| "Set"
-| "Prop"
+decl_notation: [
+| ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 ]
 
-universe_expr: [
-| universe_name universe_increment
+decl_sep: [
+| "and"
 ]
 
-universe: [
-| "max" "(" LIST1 universe_expr SEP "," ")"
-| universe_expr
+decl_notations: [
+| "where" LIST1 decl_notation SEP decl_sep
+|
 ]
 
-lconstr: [
-| term200
+opt_constructors_or_fields: [
+| ":=" constructors_or_record
+|
 ]
 
-constr: [
-| term8
-| "@" global univ_annot
+inductive_definition: [
+| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations
 ]
 
-term200: [
-| binder_constr
-| term100
+constructors_or_record: [
+| "|" LIST1 constructor SEP "|"
+| identref constructor_type "|" LIST1 constructor SEP "|"
+| identref constructor_type
+| identref "{" record_fields "}"
+| "{" record_fields "}"
+|
 ]
 
-term100: [
-| term99 "<:" term200
-| term99 "<<:" term200
-| term99 ":" term200
-| term99 ":>"
-| term99
+opt_coercion: [
+| ">"
+|
 ]
 
-term99: [
-| term90
+fix_definition: [
+| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
-term90: [
-| term10
+cofix_definition: [
+| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations
 ]
 
-term10: [
-| term9 LIST1 arg
-| "@" global univ_annot LIST0 term9
-| "@" pattern_ident LIST1 identref
-| term9
+scheme: [
+| scheme_kind
+| identref ":=" scheme_kind
 ]
 
-term9: [
-| ".." term0 ".."
-| term8
+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
 ]
 
-term8: [
-| term1
+record_field: [
+| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations
 ]
 
-term1: [
-| term0 ".(" global LIST0 arg ")"
-| term0 ".(" "@" global LIST0 ( term9 ) ")"
-| term0 "%" IDENT
-| term0
+record_fields: [
+| record_field ";" record_fields
+| record_field
+|
 ]
 
-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 ")"
+field_body: [
+| binders of_type lconstr
+| binders of_type lconstr ":=" lconstr
+| binders ":=" lconstr
 ]
 
-array_elems: [
-| LIST0 lconstr SEP ";"
+record_binder: [
+| name
+| name field_body
 ]
 
-record_declaration: [
-| fields_def
+assum_list: [
+| LIST1 assum_coe
+| assumpt
 ]
 
-fields_def: [
-| field_def ";" fields_def
-| field_def
-|
+assum_coe: [
+| "(" assumpt ")"
 ]
 
-field_def: [
-| global binders ":=" lconstr
+assumpt: [
+| LIST1 ident_decl of_type lconstr
 ]
 
-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 *)
+constructor_type: [
+| binders [ of_type lconstr | ]
 ]
 
-arg: [
-| test_lpar_id_coloneq "(" identref ":=" lconstr ")"
-| term9
+constructor: [
+| identref constructor_type
 ]
 
-atomic_constr: [
-| global univ_annot
-| sort
-| NUMBER
-| string
-| "_"
-| "?" "[" identref "]"
-| "?" "[" pattern_ident "]"
-| pattern_ident evar_instance
+of_type: [
+| ":>"
+| ":" ">"
+| ":"
 ]
 
-inst: [
-| identref ":=" lconstr
+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 *)
 ]
 
-evar_instance: [
-| "@{" LIST1 inst SEP ";" "}"
-|
+filtered_import: [
+| global
+| global "(" LIST1 one_import_filter_name SEP "," ")"
 ]
 
-univ_annot: [
-| "@{" LIST0 universe_level "}"
-|
+one_import_filter_name: [
+| global OPT [ "(" ".." ")" ]
 ]
 
-universe_level: [
-| "Set"
-| "Prop"
-| "Type"
-| "_"
-| global
+export_token: [
+| "Import"
+| "Export"
+|
 ]
 
-fix_decls: [
-| fix_decl
-| fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
+ext_module_type: [
+| "<+" module_type_inl
 ]
 
-cofix_decls: [
-| cofix_body
-| cofix_body "with" LIST1 cofix_body SEP "with" "for" identref
+ext_module_expr: [
+| "<+" module_expr_inl
 ]
 
-fix_decl: [
-| identref binders_fixannot type_cstr ":=" term200
+check_module_type: [
+| "<:" module_type_inl
 ]
 
-cofix_body: [
-| identref binders type_cstr ":=" term200
+check_module_types: [
+| LIST0 check_module_type
 ]
 
-term_match: [
-| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end"
+of_module_type: [
+| ":" module_type_inl
+| check_module_types
 ]
 
-case_item: [
-| term100 OPT [ "as" name ] OPT [ "in" pattern200 ]
+is_module_type: [
+| ":=" module_type_inl LIST0 ext_module_type
+|
 ]
 
-case_type: [
-| "return" term100
+is_module_expr: [
+| ":=" module_expr_inl LIST0 ext_module_expr
+|
 ]
 
-as_return_type: [
-| OPT [ OPT [ "as" name ] case_type ]
+functor_app_annot: [
+| "[" "inline" "at" "level" natural "]"
+| "[" "no" "inline" "]"
+|
 ]
 
-branches: [
-| OPT "|" LIST0 eqn SEP "|"
+module_expr_inl: [
+| "!" module_expr
+| module_expr functor_app_annot
 ]
 
-mult_pattern: [
-| LIST1 pattern200 SEP ","
+module_type_inl: [
+| "!" module_type
+| module_type functor_app_annot
 ]
 
-eqn: [
-| LIST1 mult_pattern SEP "|" "=>" lconstr
+module_binder: [
+| "(" export_token LIST1 identref ":" module_type_inl ")"
 ]
 
-record_pattern: [
-| global ":=" pattern200
+module_expr: [
+| module_expr_atom
+| module_expr module_expr_atom
 ]
 
-record_patterns: [
-| record_pattern ";" record_patterns
-| record_pattern
-|
+module_expr_atom: [
+| qualid
+| "(" module_expr ")"
 ]
 
-pattern200: [
-| pattern100
+with_declaration: [
+| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
+| "Module" fullyqualid ":=" qualid
 ]
 
-pattern100: [
-| pattern99 ":" term200
-| pattern99
+module_type: [
+| qualid
+| "(" module_type ")"
+| module_type module_expr_atom
+| module_type "with" with_declaration
 ]
 
-pattern99: [
-| pattern90
+section_subset_expr: [
+| test_only_starredidentrefs LIST0 starredidentref
+| ssexpr35
 ]
 
-pattern90: [
-| pattern10
+starredidentref: [
+| identref
+| identref "*"
+| "Type"
+| "Type" "*"
 ]
 
-pattern10: [
-| pattern1 "as" name
-| pattern1 LIST1 pattern1
-| "@" Prim.reference LIST0 pattern1
-| pattern1
+ssexpr35: [
+| "-" ssexpr50
+| ssexpr50
 ]
 
-pattern1: [
-| pattern0 "%" IDENT
-| pattern0
+ssexpr50: [
+| ssexpr0 "-" ssexpr0
+| ssexpr0 "+" ssexpr0
+| ssexpr0
 ]
 
-pattern0: [
-| Prim.reference
-| "{|" record_patterns bar_cbrace
-| "_"
-| "(" pattern200 ")"
-| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
-| NUMBER
-| string
+ssexpr0: [
+| starredidentref
+| "(" test_only_starredidentrefs LIST0 starredidentref ")"
+| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*"
+| "(" ssexpr35 ")"
+| "(" ssexpr35 ")" "*"
 ]
 
-fixannot: [
-| "{" "struct" identref "}"
-| "{" "wf" constr identref "}"
-| "{" "measure" constr OPT identref OPT constr "}"
+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"
 ]
 
-binders_fixannot: [
-| ensure_fixannot fixannot
-| binder binders_fixannot
-|
+scope_delimiter: [
+| "%" IDENT
 ]
 
-open_binders: [
-| name LIST0 name ":" lconstr
-| name LIST0 name binders
-| name ".." name
-| closed_binder binders
+argument_spec: [
+| OPT "!" name OPT scope_delimiter
 ]
 
-binders: [
-| LIST0 binder
-| Pcoq.Constr.binders
+arg_specs: [
+| argument_spec
+| "/"
+| "&"
+| "(" LIST1 argument_spec ")" OPT scope_delimiter
+| "[" LIST1 argument_spec "]" OPT scope_delimiter
+| "{" LIST1 argument_spec "}" OPT scope_delimiter
 ]
 
-binder: [
+implicits_alt: [
 | name
-| closed_binder
+| "[" LIST1 name "]"
+| "{" LIST1 name "}"
 ]
 
-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 *)
+instance_name: [
+| ident_decl binders
+|
 ]
 
-one_open_binder: [
-| name
-| name ":" lconstr
-| one_closed_binder
+hint_info: [
+| "|" OPT natural OPT constr_pattern
+|
+]
+
+reserv_list: [
+| LIST1 reserv_tuple
+| simple_reserv
 ]
 
-one_closed_binder: [
-| "(" name ":" lconstr ")"
-| "{" name "}"
-| "{" name ":" lconstr "}"
-| "[" name "]"
-| "[" name ":" lconstr "]"
-| "'" pattern0
+reserv_tuple: [
+| "(" simple_reserv ")"
 ]
 
-typeclass_constraint: [
-| "!" term200
-| "{" name "}" ":" [ "!" | ] term200
-| test_name_colon name ":" [ "!" | ] term200
-| term200
+simple_reserv: [
+| LIST1 identref ":" lconstr
 ]
 
-type_cstr: [
-| ":" lconstr
-|
+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 "."
 ]
 
-let_type_cstr: [
-| OPT [ ":" lconstr ]
+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"
 ]
 
-preident: [
-| IDENT
+printunivs_subgraph: [
+| "Subgraph" "(" LIST0 reference ")"
 ]
 
-ident: [
-| IDENT
+class_rawexpr: [
+| "Funclass"
+| "Sortclass"
+| smart_global
 ]
 
-pattern_ident: [
-| LEFTQMARK ident
+locatable: [
+| smart_global
+| "Term" smart_global
+| "File" ne_string
+| "Library" global
+| "Module" global
 ]
 
-identref: [
-| ident
+option_setting: [
+|
+| integer
+| STRING
 ]
 
-hyp: [
-| identref
+table_value: [
+| global
+| STRING
 ]
 
-field: [
-| FIELD
+setting_name: [
+| LIST1 IDENT
 ]
 
-fields: [
-| field fields
-| field
+ne_in_or_out_modules: [
+| "inside" LIST1 global
+| "outside" LIST1 global
 ]
 
-fullyqualid: [
-| ident fields
-| ident
+in_or_out_modules: [
+| ne_in_or_out_modules
+|
 ]
 
-name: [
-| "_"
-| ident
+comment: [
+| constr
+| STRING
+| natural
 ]
 
-reference: [
-| ident fields
-| ident
+positive_search_mark: [
+| "-"
+|
 ]
 
-qualid: [
-| reference
+search_query: [
+| positive_search_mark search_item
+| positive_search_mark "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
 ]
 
-by_notation: [
-| ne_string OPT [ "%" 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
 ]
 
-smart_global: [
-| reference
-| by_notation
+logical_kind: [
+| thm_token
+| assumption_token
+| "Context"
+| extended_def_token
+| "Primitive"
 ]
 
-ne_string: [
-| STRING
+extended_def_token: [
+| def_token
+| "Coercion"
+| "Instance"
+| "Scheme"
+| "Canonical"
+| "Field"
+| "Method"
 ]
 
-ne_lstring: [
-| ne_string
+search_where: [
+| "head"
+| "hyp"
+| "concl"
+| "headhyp"
+| "headconcl"
 ]
 
-dirpath: [
-| ident LIST0 field
+search_queries: [
+| ne_in_or_out_modules
+| search_query search_queries
+|
 ]
 
-string: [
-| STRING
+univ_name_list: [
+| "@{" LIST0 name "}"
 ]
 
-lstring: [
-| string
+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
 ]
 
-integer: [
-| bigint
+only_parsing: [
+| "(" "only" "parsing" ")"
+|
 ]
 
-natural: [
-| bignat
+level: [
+| "level" natural
+| "next" "level"
 ]
 
-bigint: [
-| bignat
-| test_minus_nat "-" bignat
+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
 ]
 
-bignat: [
-| NUMBER
+syntax_modifiers: [
+| "(" LIST1 syntax_modifier SEP "," ")"
+|
 ]
 
-bar_cbrace: [
-| test_pipe_closedcurly "|" "}"
+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
 ]
 
-strategy_level: [
-| "expand"
-| "opaque"
-| integer
-| "transparent"
+at_level_opt: [
+| "at" level
+|
+]
+
+binder_interp: [
+| "as" "ident"
+| "as" "name"
+| "as" "pattern"
+| "as" "strict" "pattern"
 ]
 
 simple_tactic: [
@@ -3283,7 +3283,7 @@ ltac2_expr6: [
 ]
 
 ltac2_expr5: [
-| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6      (* Ltac2 plugin *)
+| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" ltac2_expr6      (* Ltac2 plugin *)
 | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
 | "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
@@ -3371,8 +3371,13 @@ tac2expr_in_env: [
 | ltac2_expr6      (* Ltac2 plugin *)
 ]
 
+type_cast: [
+|      (* Ltac2 plugin *)
+| ":" ltac2_type5      (* Ltac2 plugin *)
+]
+
 G_LTAC2_let_clause: [
-| let_binder ":=" ltac2_expr6      (* Ltac2 plugin *)
+| let_binder type_cast ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 let_binder: [
@@ -3415,7 +3420,7 @@ G_LTAC2_input_fun: [
 ]
 
 tac2def_body: [
-| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6      (* Ltac2 plugin *)
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6      (* Ltac2 plugin *)
 ]
 
 tac2def_val: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 5674d28139..5b19b7fc55 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -2274,7 +2274,7 @@ ltac2_entry: [
 ]
 
 tac2def_body: [
-| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr      (* Ltac2 plugin *)
 ]
 
 tac2typ_def: [
@@ -2315,13 +2315,13 @@ ltac2_expr: [
 ]
 
 ltac2_expr5: [
-| "fun" LIST1 tac2pat0 "=>" ltac2_expr      (* Ltac2 plugin *)
+| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr      (* Ltac2 plugin *)
 | "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr      (* Ltac2 plugin *)
 | ltac2_expr3      (* Ltac2 plugin *)
 ]
 
 ltac2_let_clause: [
-| LIST1 tac2pat0 ":=" ltac2_expr      (* Ltac2 plugin *)
+| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr      (* Ltac2 plugin *)
 ]
 
 ltac2_expr3: [
-- 
cgit v1.2.3