diff options
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 719 |
1 files changed, 684 insertions, 35 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 20ac8f8bf3..a787d769fb 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -119,6 +119,7 @@ term0: [ | "`{" term200 "}" | test_array_opening "[" "|" array_elems "|" lconstr type_cstr test_array_closing "|" "]" univ_annot | "`(" term200 ")" +| "ltac" ":" "(" Pltac.ltac_expr ")" ] array_elems: [ @@ -152,6 +153,11 @@ binder_constr: [ | "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 *) ] arg: [ @@ -308,6 +314,7 @@ open_binders: [ binders: [ | LIST0 binder +| Pcoq.Constr.binders ] binder: [ @@ -332,6 +339,7 @@ closed_binder: [ | "`{" LIST1 typeclass_constraint SEP "," "}" | "`[" LIST1 typeclass_constraint SEP "," "]" | "'" pattern0 +| [ "of" | "&" ] term99 (* SSR plugin *) ] typeclass_constraint: [ @@ -632,20 +640,20 @@ command: [ | "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" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident -| "Add" "Parametric" "Relation" G_REWRITE_binders ":" 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" G_REWRITE_binders ":" 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" G_REWRITE_binders ":" 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" @@ -686,6 +694,10 @@ command: [ | "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 @@ -713,6 +725,7 @@ hint: [ | "Mode" global mode | "Unfold" LIST1 global | "Constructors" LIST1 global +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic ] constr_body: [ @@ -746,6 +759,7 @@ attribute_list: [ attribute: [ | ident attr_value +| "using" attr_value ] attr_value: [ @@ -1021,6 +1035,7 @@ gallina_ext: [ | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | "Export" "Set" setting_name option_setting | "Export" "Unset" setting_name +| "Import" "Prenex" "Implicits" (* SSR plugin *) ] filtered_import: [ @@ -1743,6 +1758,51 @@ simple_tactic: [ | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "rtauto" +| "by" ssrhintarg (* SSR plugin *) +| "clear" natural (* SSR plugin *) +| "move" ssrmovearg ssrrpat (* SSR plugin *) +| "move" ssrmovearg ssrclauses (* SSR plugin *) +| "move" ssrrpat (* SSR plugin *) +| "move" (* SSR plugin *) +| "case" ssrcasearg ssrclauses (* SSR plugin *) +| "case" (* SSR plugin *) +| "elim" ssrarg ssrclauses (* SSR plugin *) +| "elim" (* SSR plugin *) +| "apply" ssrapplyarg (* SSR plugin *) +| "apply" (* SSR plugin *) +| "exact" ssrexactarg (* SSR plugin *) +| "exact" (* SSR plugin *) +| "exact" "<:" lconstr (* SSR plugin *) +| "congr" ssrcongrarg (* SSR plugin *) +| "ssrinstancesofruleL2R" ssrterm (* SSR plugin *) +| "ssrinstancesofruleR2L" ssrterm (* SSR plugin *) +| "rewrite" ssrrwargs ssrclauses (* SSR plugin *) +| "unlock" ssrunlockargs ssrclauses (* SSR plugin *) +| "pose" ssrfixfwd (* SSR plugin *) +| "pose" ssrcofixfwd (* SSR plugin *) +| "pose" ssrfwdid ssrposefwd (* SSR plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* SSR plugin *) +| "abstract" ssrdgens (* SSR plugin *) +| "have" ssrhavefwdwbinders (* SSR plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* SSR plugin *) +| "suff" ssrsufffwd (* SSR plugin *) +| "suffices" ssrsufffwd (* SSR plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* SSR plugin *) +| "under" ssrrwarg (* SSR plugin *) +| "under" ssrrwarg ssrintros_ne (* SSR plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* SSR plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* SSR plugin *) +| "ssrinstancesoftpat" G_SSRMATCHING_cpattern (* SSR plugin *) ] mlname: [ @@ -1763,9 +1823,7 @@ language: [ ] firstorder_using: [ -| "using" reference -| "using" reference "," LIST1 reference SEP "," -| "using" reference reference LIST0 reference +| "using" LIST1 reference SEP "," | ] @@ -1849,6 +1907,10 @@ by_arg_tac: [ in_clause: [ | in_clause' +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," ] test_lpar_id_colon: [ @@ -1950,6 +2012,9 @@ ltac_expr4: [ | ltac_expr3 ";" ltac_expr3 | ltac_expr3 ";" tactic_then_locality for_each_goal "]" | ltac_expr3 +| ltac_expr5 ";" "first" ssr_first_else (* SSR plugin *) +| ltac_expr5 ";" "first" ssrseqarg (* SSR plugin *) +| ltac_expr5 ";" "last" ssrseqarg (* SSR plugin *) ] ltac_expr3: [ @@ -1966,6 +2031,10 @@ ltac_expr3: [ | "abstract" ltac_expr2 "using" ident | "only" selector ":" ltac_expr3 | ltac_expr2 +| "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "do" ssrortacarg ssrclauses (* SSR plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "abstract" ssrdgens (* SSR plugin *) ] ltac_expr2: [ @@ -1989,12 +2058,14 @@ ltac_expr1: [ | tactic_value | reference LIST0 tactic_arg | ltac_expr0 +| ltac_expr5 ssrintros_ne (* SSR plugin *) ] ltac_expr0: [ | "(" ltac_expr5 ")" | "[" ">" for_each_goal "]" | tactic_atom +| ssrparentacarg (* SSR plugin *) ] failkw: [ @@ -2139,14 +2210,6 @@ tactic_mode: [ | "par" ":" OPT ltac_info tactic ltac_use_default ] -G_LTAC_hint: [ -| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic -] - -G_LTAC_term0: [ -| "ltac" ":" "(" Pltac.ltac_expr ")" -] - ltac_selector: [ | toplevel_selector ] @@ -2217,10 +2280,6 @@ rewstrategy: [ | "fold" constr ] -G_REWRITE_binders: [ -| Pcoq.Constr.binders -] - int_or_var: [ | integer | identref @@ -2393,32 +2452,27 @@ hypident: [ | id_or_meta | "(" "type" "of" id_or_meta ")" | "(" "value" "of" id_or_meta ")" +| "(" "type" "of" Prim.identref ")" (* SSR plugin *) +| "(" "value" "of" Prim.identref ")" (* SSR plugin *) ] hypident_occ: [ | hypident occs ] -G_TACTIC_in_clause: [ -| "*" occs -| "*" "|-" concl_occ -| LIST0 hypident_occ SEP "," "|-" concl_occ -| LIST0 hypident_occ SEP "," -] - clause_dft_concl: [ -| "in" G_TACTIC_in_clause +| "in" in_clause | occs | ] clause_dft_all: [ -| "in" G_TACTIC_in_clause +| "in" in_clause | ] opt_clause: [ -| "in" G_TACTIC_in_clause +| "in" in_clause | "at" occs_nums | ] @@ -2549,6 +2603,601 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] +ssrtacarg: [ +| ltac_expr5 (* SSR plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* SSR plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* SSR plugin *) +] + +ssrhyp: [ +| ident (* SSR plugin *) +] + +ssrhoi_hyp: [ +| ident (* SSR plugin *) +] + +ssrhoi_id: [ +| ident (* SSR plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* SSR plugin *) +| "/=" (* SSR plugin *) +| test_ssrslashnum11 "/" natural "/" natural "=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/=" (* SSR plugin *) +| test_ssrslashnum10 "/" natural "/" "=" (* SSR plugin *) +| test_ssrslashnum01 "//" natural "=" (* SSR plugin *) +| test_ssrslashnum00 "//" (* SSR plugin *) +] + +ssrclear_ne: [ +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +] + +ssrclear: [ +| ssrclear_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrindex: [ +] + +ssrocc: [ +| natural LIST0 natural (* SSR plugin *) +| "-" LIST0 natural (* SSR plugin *) +| "+" LIST0 natural (* SSR plugin *) +] + +ssrmmod: [ +| "!" (* SSR plugin *) +| LEFTQMARK (* SSR plugin *) +| "?" (* SSR plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* SSR plugin *) +| ssrmmod (* SSR plugin *) +] + +ssrmult: [ +| ssrmult_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* SSR plugin *) +| "{" LIST0 ssrhyp "}" (* SSR plugin *) +] + +ssrterm: [ +| ssrtermkind Pcoq.Constr.constr (* SSR plugin *) +] + +ast_closure_term: [ +| term_annotation constr (* SSR plugin *) +] + +ast_closure_lterm: [ +| term_annotation lconstr (* SSR plugin *) +] + +ssrbwdview: [ +| test_not_ssrslashnum "/" Pcoq.Constr.constr (* SSR plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview (* SSR plugin *) +] + +ssrfwdview: [ +| test_not_ssrslashnum "/" ast_closure_term (* SSR plugin *) +| test_not_ssrslashnum "/" ast_closure_term ssrfwdview (* SSR plugin *) +] + +ident_no_do: [ +| test_ident_no_do IDENT (* SSR plugin *) +] + +ssripat: [ +| "_" (* SSR plugin *) +| "*" (* SSR plugin *) +| ">" (* SSR plugin *) +| ident_no_do (* SSR plugin *) +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| "++" (* SSR plugin *) +| ssrsimpl_ne (* SSR plugin *) +| ssrdocc "->" (* SSR plugin *) +| ssrdocc "<-" (* SSR plugin *) +| ssrdocc (* SSR plugin *) +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +| "-" (* SSR plugin *) +| "-/" "=" (* SSR plugin *) +| "-/=" (* SSR plugin *) +| "-/" "/" (* SSR plugin *) +| "-//" (* SSR plugin *) +| "-/" integer "/" (* SSR plugin *) +| "-/" "/=" (* SSR plugin *) +| "-//" "=" (* SSR plugin *) +| "-//=" (* SSR plugin *) +| "-/" integer "/=" (* SSR plugin *) +| "-/" integer "/" integer "=" (* SSR plugin *) +| ssrfwdview (* SSR plugin *) +| "[" ":" LIST0 ident "]" (* SSR plugin *) +| "[:" LIST0 ident "]" (* SSR plugin *) +| ssrcpat (* SSR plugin *) +] + +ssripats: [ +| ssripat ssripats (* SSR plugin *) +| (* SSR plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* SSR plugin *) +| ssripats "|-" ">" ssriorpat (* SSR plugin *) +| ssripats "|-" ssriorpat (* SSR plugin *) +| ssripats "|->" ssriorpat (* SSR plugin *) +| ssripats "||" ssriorpat (* SSR plugin *) +| ssripats "|||" ssriorpat (* SSR plugin *) +| ssripats "||||" ssriorpat (* SSR plugin *) +| ssripats (* SSR plugin *) +] + +ssrcpat: [ +| test_nohidden "[" hat "]" (* SSR plugin *) +| test_nohidden "[" ssriorpat "]" (* SSR plugin *) +| test_nohidden "[=" ssriorpat "]" (* SSR plugin *) +] + +hat: [ +| "^" ident (* SSR plugin *) +| "^" "~" ident (* SSR plugin *) +| "^" "~" natural (* SSR plugin *) +| "^~" ident (* SSR plugin *) +| "^~" natural (* SSR plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* SSR plugin *) +] + +ssrhpats: [ +| ssripats (* SSR plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* SSR plugin *) +| ssripats "@" ssripats (* SSR plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* SSR plugin *) +] + +ssrrpat: [ +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* SSR plugin *) +] + +ssrintros: [ +| ssrintros_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrintrosarg: [ +] + +ssrfwdid: [ +| test_ssrfwdid Prim.ident (* SSR plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* SSR plugin *) +| ssrtacarg "|" (* SSR plugin *) +| ssrtacarg (* SSR plugin *) +| "|" ssrortacs (* SSR plugin *) +| "|" (* SSR plugin *) +] + +ssrhintarg: [ +| "[" "]" (* SSR plugin *) +| "[" ssrortacs "]" (* SSR plugin *) +| ssrtacarg (* SSR plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* SSR plugin *) +| "[" ssrortacs "]" (* SSR plugin *) +| ssrtac3arg (* SSR plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* SSR plugin *) +] + +ssrhint: [ +| (* SSR plugin *) +| "by" ssrhintarg (* SSR plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* SSR plugin *) +| ssrhoi_hyp (* SSR plugin *) +| "@" ssrhoi_hyp (* SSR plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +| "(" ssrhoi_id ")" (* SSR plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* SSR plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* SSR plugin *) +| ssrwgen ssrclausehyps (* SSR plugin *) +| ssrwgen (* SSR plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* SSR plugin *) +| "in" ssrclausehyps "|-" (* SSR plugin *) +| "in" ssrclausehyps "*" (* SSR plugin *) +| "in" ssrclausehyps (* SSR plugin *) +| "in" "|-" "*" (* SSR plugin *) +| "in" "*" (* SSR plugin *) +| "in" "*" "|-" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* SSR plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrbvar: [ +| ident (* SSR plugin *) +| "_" (* SSR plugin *) +] + +ssrbinder: [ +| ssrbvar (* SSR plugin *) +| "(" ssrbvar ")" (* SSR plugin *) +| "(" ssrbvar ":" lconstr ")" (* SSR plugin *) +| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* SSR plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* SSR plugin *) +| "(" ssrbvar ":=" lconstr ")" (* SSR plugin *) +| [ "of" | "&" ] term99 (* SSR plugin *) +] + +ssrstruct: [ +| "{" "struct" ident "}" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrposefwd: [ +| LIST0 ssrbinder ssrfwd (* SSR plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd (* SSR plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar LIST0 ssrbinder ssrfwd (* SSR plugin *) +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* SSR plugin *) +| ":=" "{" ssrocc "}" cpattern (* SSR plugin *) +| ":=" lcpattern (* SSR plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* SSR plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* SSR plugin *) +| ":" ast_closure_lterm ":=" (* SSR plugin *) +| ":=" ast_closure_lterm (* SSR plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* SSR plugin *) +] + +ssrdoarg: [ +] + +ssrseqarg: [ +| ssrswap (* SSR plugin *) +| ssrseqidx ssrortacarg OPT ssrorelse (* SSR plugin *) +| ssrseqidx ssrswap (* SSR plugin *) +| ltac_expr3 (* SSR plugin *) +] + +ssrseqidx: [ +| test_ssrseqvar Prim.ident (* SSR plugin *) +| Prim.natural (* SSR plugin *) +] + +ssrswap: [ +| "first" (* SSR plugin *) +| "last" (* SSR plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* SSR plugin *) +] + +Prim.ident: [ +| IDENT ssr_null_entry (* SSR plugin *) +] + +ssrparentacarg: [ +| "(" ltac_expr5 ")" (* SSR plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* SSR plugin *) +| ssrortacarg (* SSR plugin *) +] + +ssrseqdir: [ +] + +ssr_first: [ +| ssr_first ssrintros_ne (* SSR plugin *) +| "[" LIST0 ltac_expr5 SEP "|" "]" (* SSR plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* SSR plugin *) +| ssr_first (* SSR plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* SSR plugin *) +| cpattern (* SSR plugin *) +] + +ssrdgens_tl: [ +| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl (* SSR plugin *) +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* SSR plugin *) +| "/" ssrdgens_tl (* SSR plugin *) +| cpattern ssrdgens_tl (* SSR plugin *) +| (* SSR plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* SSR plugin *) +] + +ssreqid: [ +| test_ssreqid ssreqpat (* SSR plugin *) +| test_ssreqid (* SSR plugin *) +] + +ssreqpat: [ +| Prim.ident (* SSR plugin *) +| "_" (* SSR plugin *) +| "?" (* SSR plugin *) +| "+" (* SSR plugin *) +| ssrdocc "->" (* SSR plugin *) +| ssrdocc "<-" (* SSR plugin *) +| "->" (* SSR plugin *) +| "<-" (* SSR plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* SSR plugin *) +| ssrfwdview ssrclear ssrintros (* SSR plugin *) +| ssreqid ssrdgens ssrintros (* SSR plugin *) +| ssrclear_ne ssrintros (* SSR plugin *) +| ssrintros_ne (* SSR plugin *) +] + +ssrmovearg: [ +| ssrarg (* SSR plugin *) +] + +ssrcasearg: [ +| ssrarg (* SSR plugin *) +] + +ssragen: [ +| "{" LIST1 ssrhyp "}" ssrterm (* SSR plugin *) +| ssrterm (* SSR plugin *) +] + +ssragens: [ +| "{" LIST1 ssrhyp "}" ssrterm ssragens (* SSR plugin *) +| "{" LIST1 ssrhyp "}" (* SSR plugin *) +| ssrterm ssragens (* SSR plugin *) +| (* SSR plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* SSR plugin *) +| ssrclear_ne ssrintros (* SSR plugin *) +| ssrintros_ne (* SSR plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* SSR plugin *) +| ssrbwdview ssrclear ssrintros (* SSR plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* SSR plugin *) +| ssrbwdview ssrclear (* SSR plugin *) +| ssrclear_ne (* SSR plugin *) +] + +ssrcongrarg: [ +| natural constr ssrdgens (* SSR plugin *) +| natural constr (* SSR plugin *) +| constr ssrdgens (* SSR plugin *) +| constr (* SSR plugin *) +] + +ssrrwocc: [ +| "{" LIST0 ssrhyp "}" (* SSR plugin *) +| "{" ssrocc "}" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrrule_ne: [ +| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* SSR plugin *) +| ssrsimpl_ne (* SSR plugin *) +] + +ssrrule: [ +| ssrrule_ne (* SSR plugin *) +| (* SSR plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* SSR plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "-/" ssrterm (* SSR plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| "{" LIST1 ssrhyp "}" ssrrule (* SSR plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* SSR plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* SSR plugin *) +| ssrrule_ne (* SSR plugin *) +] + +ssrrwargs: [ +| test_ssr_rw_syntax LIST1 ssrrwarg (* SSR plugin *) +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* SSR plugin *) +| ssrterm (* SSR plugin *) +] + +ssrunlockargs: [ +| LIST0 ssrunlockarg (* SSR plugin *) +] + +ssrsufffwd: [ +| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint (* SSR plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 ssrwgen "/" ast_closure_lterm (* SSR plugin *) +] + +ssr_idcomma: [ +| (* SSR plugin *) +| test_idcomma [ IDENT | "_" ] "," (* SSR plugin *) +] + +ssr_rtype: [ +| "return" term100 (* SSR plugin *) +] + +ssr_mpat: [ +| pattern200 (* SSR plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* SSR plugin *) +| ssr_mpat ssr_rtype (* SSR plugin *) +| ssr_mpat (* SSR plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* SSR plugin *) +] + +ssr_elsepat: [ +| "else" (* SSR plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* SSR plugin *) +] + +ssrhintref: [ +| constr (* SSR plugin *) +| constr "|" natural (* SSR plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* SSR plugin *) +| "for" "apply" "/" (* SSR plugin *) +| "for" "apply" "/" "/" (* SSR plugin *) +| "for" "apply" "//" (* SSR plugin *) +| (* SSR plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* SSR plugin *) +] + +rpattern: [ +| lconstr (* SSR plugin *) +| "in" lconstr (* SSR plugin *) +| lconstr "in" lconstr (* SSR plugin *) +| "in" lconstr "in" lconstr (* SSR plugin *) +| lconstr "in" lconstr "in" lconstr (* SSR plugin *) +| lconstr "as" lconstr "in" lconstr (* SSR plugin *) +] + +G_SSRMATCHING_cpattern: [ +| "Qed" constr (* SSR plugin *) +| ssrtermkind constr (* SSR plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* SSR plugin *) +| ssrtermkind lconstr (* SSR plugin *) +] + +ssrpatternarg: [ +| rpattern (* SSR plugin *) +] + +ssr_search_item: [ +| string (* SSR plugin *) +| string "%" preident (* SSR plugin *) +| constr_pattern (* SSR plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* SSR plugin *) +| ssr_search_item ssr_search_arg (* SSR plugin *) +| (* SSR plugin *) +] + +ssr_modlocs: [ +| (* SSR plugin *) +| "in" LIST1 modloc (* SSR plugin *) +] + +modloc: [ +| "-" global (* SSR plugin *) +| global (* SSR plugin *) +] + deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" |