Convert logic.rst to prodn

4 files changed, 1477 insertions, 135 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 76a41828f7..4ad32e15eb 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -19,7 +19,8 @@ lglob: [
 ]
 
 hint: [
-| "Extern" natural OPT constr_pattern "=>" tactic
+| REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
+| WITH "Extern" natural OPT constr_pattern "=>" tactic
 ]
 
 (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *)
@@ -28,19 +29,12 @@ strategy_level_or_var: [
 | strategy_level
 ]
 
-term0: [
-| "ltac" ":" "(" ltac_expr5 ")"
-]
-
 EXTRAARGS_natural: [ | DELETENT ]
 EXTRAARGS_lconstr:  [ | DELETENT ]
 EXTRAARGS_strategy_level: [ | DELETENT ]
-G_LTAC_hint: [ | DELETENT ]
-G_LTAC_term0: [ | DELETENT ]
 
-G_REWRITE_binders: [
+binders: [
 | DELETE Pcoq.Constr.binders
-| binders
 ]
 
 G_TACTIC_in_clause: [
@@ -50,7 +44,6 @@ G_TACTIC_in_clause: [
 ]
 
 SPLICE: [
-| G_REWRITE_binders
 | G_TACTIC_in_clause
 ]
 
@@ -92,6 +85,7 @@ RENAME: [
 | G_LTAC2_as_ipat ltac2_as_ipat
 | G_LTAC2_by_tactic ltac2_by_tactic
 | G_LTAC2_match_list ltac2_match_list
+| G_SSRMATCHING_cpattern ssr_one_term_pattern
 ]
 
 (* Renames to eliminate qualified names.
@@ -112,13 +106,14 @@ RENAME: [
 | Prim.natural natural
 | Pvernac.Vernac_.main_entry vernac_control
 | Tactic.tactic tactic
+| Pltac.ltac_expr ltac_expr5
 
   (* SSR *)
+| Pcoq.Constr.constr term
+| Prim.identref ident
 (*
 | G_vernac.def_body def_body
-| Pcoq.Constr.constr term
 | Prim.by_notation by_notation
-| Prim.identref ident
 | Prim.natural natural
 *)
 | Vernac.fix_definition fix_definition
@@ -156,11 +151,16 @@ DELETE: [
 | test_array_closing
 
   (* SSR *)
-(* | ssr_null_entry *)
-(*
+| ssr_null_entry
 | ssrtermkind  (* todo: rename as "test..." *)
-| term_annotation  (* todo: rename as "test..." *)
+| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
+| ssrseqdir
+| ssrindex
+| ssrintrosarg
+| ssrtclarg
+| term_annotation  (* todo: what is this? *)
 | test_idcomma
+| test_ident_no_do
 | test_nohidden
 | test_not_ssrslashnum
 | test_ssr_rw_syntax
@@ -171,10 +171,6 @@ DELETE: [
 | test_ssrslashnum01
 | test_ssrslashnum10
 | test_ssrslashnum11
-| test_ident_no_do
-| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
-| ssrseqdir
-*)
 
 (* unused *)
 | constr_comma_sequence'
@@ -182,8 +178,6 @@ DELETE: [
 | constr_may_eval
 ]
 
-(* ssrintrosarg: [ | DELETENT ] *)
-
 (* additional nts to be spliced *)
 
 tactic_then_last: [
@@ -262,7 +256,18 @@ binder_constr: [
 | MOVETO term_forall_or_fun "forall" open_binders "," term200
 | MOVETO term_forall_or_fun "fun" open_binders "=>" term200
 | MOVETO term_let "let" name binders let_type_cstr ":=" term200 "in" term200
+(*| MOVETO term_let "let" ":" ssr_mpat ":=" lconstr "in" lconstr  TAG SSR *)
+| DELETE "let" ":" ssr_mpat ":=" lconstr "in" lconstr  TAG SSR (* todo: restore for ssr *)
+| REPLACE "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr      (* ssr plugin *)
+| WITH "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr  TAG SSR
+| DELETE "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr      (* SSR plugin *)
+| DELETE "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr  TAG SSR  (* todo: restore for SSR *)
+(*| MOVETO term_let "let" ":" ssr_mpat OPT ( "in" pattern200 ) ":=" lconstr ssr_rtype "in" lconstr      TAG SSR*)
 | MOVETO term_if "if" term200 as_return_type "then" term200 "else" term200
+| REPLACE "if" term200 "is" ssr_dthen ssr_else
+| WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR
+| DELETE "if" term200 "isn't" ssr_dthen ssr_else
+| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else  TAG SSR  (* todo: restore for SSR *)
 | MOVETO term_fix "let" "fix" fix_decl "in" term200
 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200
 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
@@ -302,6 +307,7 @@ atomic_constr: [
 ltac_expr0: [
 | REPLACE "[" ">" for_each_goal "]"
 | WITH "[>" for_each_goal "]"
+| DELETE ssrparentacarg
 ]
 
 (* lexer token *)
@@ -465,6 +471,7 @@ closed_binder: [
 | MOVETO generalizing_binder "`(" LIST1 typeclass_constraint SEP "," ")"
 | MOVETO generalizing_binder "`{" LIST1 typeclass_constraint SEP "," "}"
 | MOVETO generalizing_binder "`[" LIST1 typeclass_constraint SEP "," "]"
+| DELETE [ "of" | "&" ] term99  (* todo: remove for SSR *)
 ]
 
 name_colon: [
@@ -565,10 +572,6 @@ finite_token: [
 | DELETENT
 ]
 
-constructors_or_record: [
-| OPTINREF
-]
-
 record_fields: [
 | REPLACE record_field ";" record_fields
 | WITH LIST0 record_field SEP ";" OPT ";"
@@ -584,11 +587,6 @@ inline: [
 | REPLACE "Inline" "(" natural ")"
 | WITH "Inline" OPT ( "(" natural ")" )
 | DELETE "Inline"
-| OPTINREF
-]
-
-univ_annot: [
-| OPTINREF
 ]
 
 univ_decl: [
@@ -604,10 +602,6 @@ of_type: [
 | [ ":" | ":>" ] type
 ]
 
-attr_value: [
-| OPTINREF
-]
-
 def_body: [
 | DELETE binders ":=" reduce lconstr
 | REPLACE binders ":" lconstr ":=" reduce lconstr
@@ -749,6 +743,7 @@ subsequent_letter: [
 
 ident: [
 | DELETE IDENT
+| DELETE IDENT (* 2nd copy from SSR *)
 | first_letter LIST0 subsequent_letter
 ]
 
@@ -804,6 +799,10 @@ ltac_expr4: [
 | REPLACE ltac_expr3 ";" binder_tactic
 | WITH ltac_expr3 ";" [ ltac_expr3 | binder_tactic ]
 | DELETE ltac_expr3 ";" ltac_expr3
+| MOVETO simple_tactic ltac_expr5 ";" "first" ssr_first_else      TAG SSR
+| MOVETO simple_tactic ltac_expr5 ";" "first" ssrseqarg      TAG SSR
+| MOVETO simple_tactic ltac_expr5 ";" "last" ssrseqarg      TAG SSR
+| DELETE simple_tactic
 ]
 
 l3_tactic: [ ]
@@ -813,6 +812,7 @@ ltac_expr3: [
 | REPLACE "abstract" ltac_expr2 "using" ident
 | WITH "abstract" ltac_expr2 OPT ( "using" ident )
 | l3_tactic
+| EDIT "do" ADD_OPT int_or_var ssrmmod ssrdotac ssrclauses  TAG SSR
 | MOVEALLBUT ltac_builtins
 | l3_tactic
 | ltac_expr2
@@ -1069,6 +1069,43 @@ simple_tactic: [
 (* in Tactic Notation: *)
 | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp )
        OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
+| REPLACE "apply" ssrapplyarg      (* SSR plugin *)
+| WITH "apply" OPT ssrapplyarg      TAG SSR
+| DELETE "apply"
+| REPLACE "elim" ssrarg ssrclauses      (* SSR plugin *)
+| WITH "elim" OPT ( ssrarg ssrclauses )  TAG SSR
+| DELETE "elim"      (* SSR plugin *)
+| REPLACE "case" ssrcasearg ssrclauses      (* SSR plugin *)
+| WITH "case" OPT ( ssrcasearg ssrclauses ) TAG SSR
+| DELETE "case"      (* SSR plugin *)
+| REPLACE "under" ssrrwarg ssrintros_ne "do" ssrhint3arg      (* SSR plugin *)
+| WITH "under" ssrrwarg OPT ssrintros_ne OPT ( "do" ssrhint3arg )  TAG SSR
+| DELETE "under" ssrrwarg      (* SSR plugin *)
+| DELETE "under" ssrrwarg ssrintros_ne      (* SSR plugin *)
+| DELETE "under" ssrrwarg "do" ssrhint3arg      (* SSR plugin *)
+| REPLACE "move" ssrmovearg ssrrpat      (* SSR plugin *)
+| WITH "move" OPT ( OPT ssrmovearg ssrrpat )   TAG SSR
+| DELETE "move" ssrrpat      (* SSR plugin *)
+| DELETE "move"      (* SSR plugin *)
+| REPLACE "suff" "have" ssrhpats_nobs ssrhavefwd      (* SSR plugin *)
+| WITH [ "suff" | "suffices" ] OPT ( "have" ssrhpats_nobs ) ssrhavefwd      TAG SSR
+| DELETE "suffices" "have" ssrhpats_nobs ssrhavefwd      (* SSR plugin *)
+| REPLACE "suff" ssrsufffwd      (* SSR plugin *)
+| WITH [ "suff" | "suffices" ] ssrsufffwd      TAG SSR
+| DELETE "suffices" ssrsufffwd      (* SSR plugin *)
+| REPLACE "have" "suff" ssrhpats_nobs ssrhavefwd      (* SSR plugin *)
+| WITH "have" [ "suff" | "suffices" ] ssrhpats_nobs ssrhavefwd      TAG SSR
+| DELETE "have" "suffices" ssrhpats_nobs ssrhavefwd      (* SSR plugin *)
+| REPLACE "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| WITH [ "gen" | "generally" ] "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      TAG SSR
+| DELETE "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| REPLACE "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| WITH [ "wlog" | "without loss" ] OPT [ "suff" | "suffices" ] ssrhpats_nobs ssrwlogfwd ssrhint      TAG SSR
+| DELETE "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| DELETE "wlog" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| DELETE "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| DELETE "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
+| DELETE "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint      (* SSR plugin *)
 ]
 
 (* todo: don't use DELETENT for this *)
@@ -1730,6 +1767,7 @@ ltac_defined_tactics: [
 | "lra"
 | "nia"
 | "nra"
+| "over"  TAG SSR
 | "split_Rabs"
 | "split_Rmult"
 | "tauto"
@@ -1741,10 +1779,12 @@ ltac_defined_tactics: [
 tactic_notation_tactics: [
 | "assert_fails" ltac_expr3
 | "assert_succeeds" ltac_expr3
+| "dintuition" OPT ltac_expr5
+| "dtauto"
 | "field" OPT ( "[" LIST1 constr "]" )
 | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )
 | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
-| "intuition" OPT ltac_expr5
+| "intuition" OPT ltac_expr5  (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *)
 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
 | "psatz" constr OPT int_or_var
 | "ring" OPT ( "[" LIST1 constr "]" )
@@ -1860,18 +1900,6 @@ SPLICE: [
 | ltac2_orient
 ]
 
-tac2typ_prm: [
-| OPTINREF
-]
-
-tac2type_body: [
-| OPTINREF
-]
-
-atomic_tac2pat: [
-| OPTINREF
-]
-
 ltac2_expr0: [
 (*
 | DELETE "(" ")" (* covered by "()" prodn *)
@@ -1964,7 +1992,7 @@ SPLICE: [
 ltac2_expr5: [
 | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2
-| MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+| MOVETO simple_tactic "match" ltac2_expr5 "with" ltac2_branches "end"      (* Ltac2 plugin *)
 | MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
 | DELETE simple_tactic
 ]
@@ -2042,6 +2070,322 @@ ltac2_expr: [
 | DELETE _ltac2_expr
 ]
 
+ssrfwdview: [
+| REPLACE "/" ast_closure_term ssrfwdview      (* SSR plugin *)
+| WITH LIST1 ( "/" ast_closure_term )  TAG SSR
+| DELETE "/" ast_closure_term      (* SSR plugin *)
+]
+
+ssrfwd: [
+| REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm      (* SSR plugin *)
+| WITH OPT ( ":" ast_closure_lterm ) ":=" ast_closure_lterm      TAG SSR
+| DELETE ":=" ast_closure_lterm      (* SSR plugin *)
+]
+
+ssrsetfwd: [
+| REPLACE ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern      (* SSR plugin *)
+| WITH OPT ( ":" ast_closure_lterm ) ":=" [ "{" ssrocc "}" cpattern | lcpattern ]      TAG SSR
+| DELETE ":" ast_closure_lterm ":=" lcpattern      (* SSR plugin *)
+| DELETE ":=" "{" ssrocc "}" cpattern      (* SSR plugin *)
+| DELETE ":=" lcpattern      (* SSR plugin *)
+]
+
+
+(* per @gares *)
+ssrdgens: [
+| REPLACE ":" ssrgen ssrdgens_tl      (* SSR plugin *)
+| WITH ":" ssrgen OPT ( "/" ssrgen )      TAG SSR
+]
+
+ssrdgens_tl: [ | DELETENT ]
+
+ssrgen: [
+| REPLACE ssrdocc cpattern      (* SSR plugin *)
+| WITH cpattern LIST0 [ LIST1 ident | cpattern ]    TAG SSR
+| DELETE cpattern      (* SSR plugin *)
+]
+
+OPTINREF: [ ]
+
+ssrortacs: [
+| EDIT ssrtacarg "|" ADD_OPT ssrortacs      (* ssr plugin *)
+| EDIT "|" ADD_OPT ssrortacs      (* ssr plugin *)
+| EDIT ADD_OPT ssrtacarg "|" OPT ssrortacs
+]
+
+ssrocc: [
+| REPLACE natural LIST0 natural      (* SSR plugin *)
+| WITH [ natural | "+" | "-" ] LIST0 natural      TAG SSR
+| DELETE "-" LIST0 natural      (* SSR plugin *)
+| DELETE "+" LIST0 natural      (* SSR plugin *)
+]
+
+ssripat: [
+| DELETE ssrdocc "->"      (* SSR plugin *)
+| DELETE ssrdocc "<-"      (* SSR plugin *)
+| REPLACE ssrdocc      (* SSR plugin *)
+| WITH ssrdocc OPT [ "->" | "<-" ]      TAG SSR
+| DELETE "->"      (* SSR plugin *)
+| DELETE "<-"      (* SSR plugin *)
+| DELETE "-/" "="      (* SSR plugin *)
+| DELETE "-/" "/"      (* SSR plugin *)
+| DELETE "-/" integer "/"      (* SSR plugin *)
+| DELETE "-/" integer "/="      (* SSR plugin *)
+| REPLACE "-/" integer "/" integer "="      (* SSR plugin *)
+| WITH "-/" integer [ "/=" | "/" | "/" integer "=" ]     TAG SSR
+| DELETE "-/" "/="      (* SSR plugin *)
+| DELETE "-//" "="      (* SSR plugin *)
+| DELETE "[" ":" LIST0 ident "]"      (* SSR plugin *)
+]
+
+ssrsimpl_ne: [
+| DELETE "/" natural "/" "="      (* SSR plugin *)
+(* parsed but not supported per @gares *)
+| DELETE "/" natural "/"      (* SSR plugin *)
+| DELETE "/" natural "="      (* SSR plugin *)
+| DELETE "//" natural "="      (* SSR plugin *)
+]
+
+hat: [
+| DELETE "^" "~" ident      (* SSR plugin *)
+| DELETE "^" "~" natural      (* SSR plugin *)
+]
+
+ssriorpat: [
+| ssripats OPT ( [ "|" | "|-" ] ssriorpat )   TAG SSR
+| DELETE OPT ssripats "|" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats "|-" ">" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats "|-" ssriorpat      (* SSR plugin *)
+(* "|->" | "||" | "|||" | "||||" are parsing hacks *)
+| DELETE OPT ssripats "|->" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats "||" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats "|||" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats "||||" ssriorpat      (* SSR plugin *)
+| DELETE OPT ssripats      (* SSR plugin *)
+]
+
+ssrbinder: [
+| REPLACE "(" ssrbvar LIST1 ssrbvar ":" lconstr ")"      (* SSR plugin *)
+| WITH "(" LIST1 ssrbvar ":" lconstr ")"      TAG SSR
+| REPLACE "(" ssrbvar ":" lconstr ":=" lconstr ")"      (* SSR plugin *)
+| WITH "(" ssrbvar OPT ( ":" lconstr ) OPT ( ":=" lconstr ) ")"      TAG SSR
+| DELETE "(" ssrbvar ")"      (* SSR plugin *)
+| DELETE "(" ssrbvar ":" lconstr ")"      (* SSR plugin *)
+| DELETE "(" ssrbvar ":=" lconstr ")"      (* SSR plugin *)
+]
+
+ssrhavefwd: [
+| REPLACE ":" ast_closure_lterm ":=" ast_closure_lterm      (* SSR plugin *)
+| WITH ":" ast_closure_lterm ":=" OPT ast_closure_lterm     TAG SSR
+| DELETE ":" ast_closure_lterm ":="      (* SSR plugin *)
+| DELETE ":=" ast_closure_lterm      (* SSR plugin *)
+]
+
+ssrmult_ne: [
+| EDIT ADD_OPT natural ssrmmod      TAG SSR
+]
+
+rpattern: [
+| REPLACE lconstr "in" lconstr "in" lconstr      (* SSR plugin *)
+| WITH OPT ( OPT ( OPT ( OPT lconstr "in" ) lconstr ) "in" ) lconstr     TAG SSR
+| DELETE lconstr      (* SSR plugin *)
+| DELETE "in" lconstr      (* SSR plugin *)
+| DELETE lconstr "in" lconstr      (* SSR plugin *)
+| DELETE "in" lconstr "in" lconstr      (* SSR plugin *)
+]
+
+ssrrule_ne: [
+| DELETE ssrsimpl_ne      (* SSR plugin *)
+| REPLACE [ "/" ssrterm | ssrterm | ssrsimpl_ne ]      (* SSR plugin *)
+| WITH [ OPT "/" ssrterm  | ssrsimpl_ne ]      TAG SSR
+]
+
+ssrunlockarg: [
+| REPLACE "{" ssrocc "}" ssrterm      (* SSR plugin *)
+| WITH OPT ( "{" ssrocc "}" ) ssrterm      TAG SSR
+| DELETE ssrterm      (* SSR plugin *)
+]
+
+ssrclauses: [
+| REPLACE "in" ssrclausehyps "|-" "*"      (* SSR plugin *)
+| WITH "in" ssrclausehyps OPT "|-" OPT "*"      TAG SSR
+| DELETE "in" ssrclausehyps "|-"      (* SSR plugin *)
+| DELETE "in" ssrclausehyps "*"      (* SSR plugin *)
+| DELETE "in" ssrclausehyps      (* SSR plugin *)
+| REPLACE "in" "|-" "*"      (* SSR plugin *)
+| WITH "in" [ "*" | "*" "|-" | "|-" "*" ]     TAG SSR
+| DELETE "in" "*"      (* SSR plugin *)
+| DELETE "in" "*" "|-"      (* SSR plugin *)
+]
+
+ssrclausehyps: [
+| REPLACE ssrwgen "," ssrclausehyps      (* SSR plugin *)
+| WITH ssrwgen LIST0 ( OPT "," ssrwgen )     TAG SSR
+| DELETE ssrwgen ssrclausehyps      (* SSR plugin *)
+| DELETE ssrwgen      (* SSR plugin *)
+]
+
+ssrwgen: [
+| DELETE ssrhoi_hyp      (* SSR plugin *)
+| REPLACE "@" ssrhoi_hyp      (* SSR plugin *)
+| WITH OPT "@" ssrhoi_hyp      TAG SSR
+| REPLACE "(" ssrhoi_id ":=" lcpattern ")"      (* SSR plugin *)
+| WITH "(" ssrhoi_id OPT ( ":=" lcpattern ) ")"      TAG SSR
+| DELETE "(" ssrhoi_id ")"      (* SSR plugin *)
+| DELETE "(" "@" ssrhoi_id ":=" lcpattern ")"      (* SSR plugin *)
+]
+
+ssrcongrarg: [
+| REPLACE natural constr ssrdgens      (* SSR plugin *)
+| WITH OPT natural constr OPT ssrdgens      TAG SSR
+| DELETE natural constr      (* SSR plugin *)
+| DELETE constr ssrdgens      (* SSR plugin *)
+| DELETE constr      (* SSR plugin *)
+]
+
+ssrviewpos: [
+| DELETE "for" "apply" "/" "/"      (* SSR plugin *)
+]
+
+ssrhintref: [
+| REPLACE constr "|" natural      (* SSR plugin *)
+| WITH constr OPT ( "|" natural )     TAG SSR
+| DELETE constr      (* SSR plugin *)
+]
+
+ssr_search_arg: [
+| REPLACE "-" ssr_search_item OPT ssr_search_arg      (* SSR plugin *)
+| WITH LIST1 ( "-" ssr_search_item )      TAG SSR
+| DELETE ssr_search_item OPT ssr_search_arg      (* SSR plugin *)
+]
+
+ssr_search_item: [
+| DELETE string      (* SSR plugin *)
+| REPLACE string "%" preident      (* SSR plugin *)
+| WITH string OPT ( "%" preident )      TAG SSR
+]
+
+modloc: [
+| REPLACE "-" global      (* SSR plugin *)
+| WITH OPT "-" global      TAG SSR
+| DELETE global
+]
+
+ssrmmod: [
+| DELETE LEFTQMARK      (* SSR plugin *)  (* duplicate *)
+]
+
+clear_switch: [
+| "{" LIST0 ident "}"
+]
+
+ssrrwocc: [
+| REPLACE "{" LIST0 ssrhyp "}"      (* SSR plugin *)
+| WITH clear_switch
+]
+
+ssrrwarg: [
+| EDIT "{" ADD_OPT ssrocc "}" OPT ssrpattern_squarep ssrrule_ne      TAG SSR
+| REPLACE "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne      (* SSR plugin *)
+| WITH OPT ( OPT ( "{" LIST1 ssrhyp "}" ) ssrpattern_ne_squarep ) ssrrule_ne      TAG SSR
+| DELETE ssrpattern_ne_squarep ssrrule_ne      (* SSR plugin *)
+| DELETE ssrrule_ne      (* SSR plugin *)
+]
+
+ssrpattern_squarep: [  (* fix inconsistency *)
+| REPLACE "[" rpattern "]"      (* SSR plugin *)
+| WITH ssrpattern_ne_squarep   TAG SSR
+]
+
+ssripats_ne: [
+| REPLACE ssripat OPT ssripats      (* SSR plugin *)
+| WITH LIST1 ssripat      TAG SSR
+]
+
+ssripats: [  (* fix inconsistency *)
+| REPLACE ssripat OPT ssripats      (* SSR plugin *)
+| WITH ssripats_ne     TAG SSR
+]
+
+lcpattern: [
+(* per @gares *)
+| DELETE "Qed" lconstr
+]
+
+ssrapplyarg: [
+| EDIT ADD_OPT ssrbwdview ":" ssragen OPT ssragens OPT ssrintros      TAG SSR
+]
+
+constr_with_bindings_arg: [
+| EDIT ADD_OPT ">" constr_with_bindings      TAG SSR
+]
+
+destruction_arg: [
+| DELETE constr_with_bindings
+]
+
+ssrhintarg: [
+| EDIT "[" ADD_OPT ssrortacs "]"      TAG SSR
+]
+
+
+ssrhint3arg: [
+| EDIT "[" ADD_OPT ssrortacs "]"      TAG SSR
+]
+
+
+ssr_first: [
+| DELETE ssr_first ssrintros_ne      (* SSR plugin *)
+| REPLACE "[" LIST0 ltac_expr5 SEP "|" "]"      (* SSR plugin *)
+| WITH "[" LIST0 ltac_expr5 SEP "|" "]" LIST0 ssrintros_ne     TAG SSR
+]
+
+ssr_first_else: [
+| EDIT ssr_first ADD_OPT ssrorelse      TAG SSR
+]
+
+ssrseqarg: [
+| EDIT ADD_OPT ssrseqidx ssrswap      TAG SSR
+]
+
+ssr_dpat: [
+| REPLACE ssr_mpat "in" pattern200 ssr_rtype      (* SSR plugin *)
+| WITH ssr_mpat OPT ( OPT ( "in" pattern200 ) ssr_rtype )      TAG SSR
+| DELETE ssr_mpat ssr_rtype      (* SSR plugin *)
+| DELETE ssr_mpat      (* SSR plugin *)
+]
+
+ssr_one_term_pattern: [
+| DELETE "Qed" constr
+]
+
+ssrarg: [
+| EDIT ADD_OPT ssrfwdview OPT ssreqid ssrdgens OPT ssrintros      (* SSR plugin *)
+]
+
+ssragen: [
+| REPLACE "{" LIST1 ssrhyp "}" ssrterm      (* SSR plugin *)
+| WITH OPT ( "{" LIST1 ssrhyp "}" ) ssrterm      TAG SSR
+| DELETE ssrterm      (* SSR plugin *)
+]
+
+ssrbinder: [
+| REPLACE [ "of" | "&" ] term99      (* SSR plugin *)
+| WITH "of" term99      TAG SSR
+| "&" term99      TAG SSR
+]
+
+firstorder_rhs: [
+| DELETE OPT firstorder_using
+| DELETE "with" LIST1 preident
+| REPLACE OPT firstorder_using "with" LIST1 preident
+| WITH OPT firstorder_using OPT ( "with" LIST1 preident )
+]
+
+attribute: [
+| DELETE "using" OPT attr_value
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2077,18 +2421,16 @@ SPLICE: [
 | bar_cbrace
 | lconstr
 
-(*
+(* SSR *)
 | ast_closure_term
 | ast_closure_lterm
 | ident_no_do
 | ssrterm
 | ssrtacarg
 | ssrtac3arg
-| ssrtclarg
 | ssrhyp
 | ssrhoi_hyp
 | ssrhoi_id
-| ssrindex
 | ssrhpats
 | ssrhpats_nobs
 | ssrfwdid
@@ -2103,11 +2445,34 @@ SPLICE: [
 | ssrcofixfwd
 | ssrfixfwd
 | ssrhavefwdwbinders
-| ssripats_ne
 | ssrparentacarg
 | ssrposefwd
-*)
-
+| ssrstruct
+| ssrrpat
+| ssrhint
+| ssrpattern_squarep
+| ssrhintref
+| ssr_search_item
+| ssr_modlocs
+| modloc
+| ssrexactarg
+| ssrclear
+| ssrmult
+| ssripats
+| ssrintros
+| ssrrule
+| ssrpattern_squarep
+| ssrcongrarg
+| ssrdotac
+| ssrunlockarg
+| ssr_search_arg
+| ssrortacarg
+| ssrsetfwd
+| ssr_idcomma
+| ssr_dthen
+| ssr_else
+| ssr_rtype
+| ssreqid
 | preident
 | lpar_id_coloneq
 | binders
@@ -2240,6 +2605,8 @@ SPLICE: [
 | mut_flag
 | tac2rec_fieldexprs
 | syn_level
+| firstorder_rhs
+| firstorder_using
 ] (* end SPLICE *)
 
 RENAME: [
@@ -2269,6 +2636,22 @@ RENAME: [
 | ltac2_type5 ltac2_type
 | ltac2_expr6 ltac2_expr
 | starredidentref starred_ident_ref
+| ssrocc ssr_occurrences
+| ssrsimpl_ne s_item
+| ssrclear_ne ssrclear
+| ssrmult_ne mult
+| ssripats_ne ssripats
+| ssrrule_ne r_item
+| ssrintros_ne ssrintros
+| ssrpattern_ne_squarep ssrpattern_squarep
+| ssrrwarg rewrite_item
+| ssrrwocc occ_or_clear
+| rpattern rewrite_pattern
+| ssripat i_item
+| ssrwgen gen_item
+| ssrfwd ssrdefbody
+| ssrclauses ssr_in
+| ssrcpat ssrblockpat
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 548ca7364c..92a745c863 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -12,12 +12,14 @@ open Coqpp_parser
 open Coqpp_ast
 
 let exit_code = ref 0
+let error_count = ref 0
 let show_warn = ref true
 
 let fprintf = Printf.fprintf
 
 let error s =
   exit_code := 1;
+  incr error_count;
   Printf.eprintf "Error: ";
   Printf.eprintf s
 
@@ -359,10 +361,9 @@ and prod_to_prodn prod = String.concat " " (prod_to_prodn_r prod)
 let get_tag file prod =
   List.fold_left (fun rv sym ->
       match sym with
-        (* todo: temporarily limited to Ltac2 tags in prodn when not in ltac2.rst *)
-      | Sedit2 ("TAG", s2)
-        when (s2 = "Ltac2" || s2 = "not Ltac2") &&
-            file <> "doc/sphinx/proof-engine/ltac2.rst" -> "   " ^ s2
+        (* todo: only Ltac2 and SSR for now, outside of their main chapters *)
+      | Sedit2 ("TAG", "Ltac2") when file <> "doc/sphinx/proof-engine/ltac2.rst" -> "   Ltac2"
+      | Sedit2 ("TAG", "SSR") when file <> "doc/sphinx/proof-engine/ssreflect-proof-language.rst" -> "   SSR"
       | _ -> rv
     ) "" prod
 
@@ -559,6 +560,10 @@ let level_regex = Str.regexp "[a-zA-Z0-9_]*$"
 let get_plugin_name file =
   if file = "user-contrib/Ltac2/g_ltac2.mlg" then
     "Ltac2"
+  (* todo: would be better if g_search.mlg has an "ssr" prefix *)
+  else if List.mem file ["plugins/ssr/ssrparser.mlg"; "plugins/ssr/ssrvernac.mlg";
+      "plugins/ssrmatching/g_ssrmatching.mlg"; "plugins/ssrsearch/g_search.mlg"] then
+    "SSR"
   else if Str.string_match plugin_regex file 0 then
     Str.matched_group 1 file
   else
@@ -568,12 +573,12 @@ let read_mlg g is_edit ast file level_renames symdef_map =
   let res = ref [] in
   let locals = ref StringSet.empty in
   let dup_renames = ref StringMap.empty in
-  let add_prods nt prods =
+  let add_prods nt prods gramext_globals =
     if not is_edit then
-      if NTMap.mem nt !g.map && nt <> "command" && nt <> "simple_tactic" then begin
+      if NTMap.mem nt !g.map && not (List.mem nt gramext_globals) && nt <> "command" && nt <> "simple_tactic" then begin
         let new_name = String.uppercase_ascii (Filename.remove_extension (Filename.basename file)) ^ "_" ^ nt in
         dup_renames := StringMap.add nt new_name !dup_renames;
-        Printf.printf "** dup sym %s -> %s in %s\n" nt new_name file
+        if false then Printf.printf "** dup local sym %s -> %s in %s\n" nt new_name file
       end;
       add_symdef nt file symdef_map;
     let plugin = get_plugin_name file in
@@ -594,11 +599,12 @@ let read_mlg g is_edit ast file level_renames symdef_map =
         | Some s -> s
         | None -> ""
       in
+      let gramext_globals = ref grammar_ext.gramext_globals in
       List.iter (fun ent ->
           let len = List.length ent.gentry_rules in
           List.iteri (fun i rule ->
               let nt = ent.gentry_name in
-              if not (List.mem nt grammar_ext.gramext_globals) then
+              if not (List.mem nt !gramext_globals) then
                 locals := StringSet.add nt !locals;
               let level = (get_label rule.grule_label) in
               let level = if level <> "" then level else
@@ -629,8 +635,11 @@ let read_mlg g is_edit ast file level_renames symdef_map =
                 if cur_level <> nt && i+1 < len then
                   edited @ [[Snterm next_level]]
                 else
-                  edited in
-              add_prods cur_level prods_to_add)
+                  edited
+              in
+              if cur_level <> nt && List.mem nt !gramext_globals then
+                gramext_globals := cur_level :: !gramext_globals;
+              add_prods cur_level prods_to_add !gramext_globals)
             ent.gentry_rules
         ) grammar_ext.gramext_entries
 
@@ -640,16 +649,16 @@ let read_mlg g is_edit ast file level_renames symdef_map =
       | Some c -> String.trim c.code
       in
       add_prods node
-        (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules)
+        (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) []
     | VernacArgumentExt vernac_argument_ext ->
       add_prods vernac_argument_ext.vernacargext_name
-        (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules)
+        (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) []
     | TacticExt tactic_ext ->
       add_prods "simple_tactic"
-        (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules)
+        (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) []
     | ArgumentExt argument_ext ->
       add_prods argument_ext.argext_name
-        (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules)
+        (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) []
     | _ -> ()
   in
 
@@ -1910,7 +1919,10 @@ let process_rst g file args seen tac_prods cmd_prods =
 
   let cmd_exclude_files = [
     "doc/sphinx/proof-engine/ssreflect-proof-language.rst";
-    "doc/sphinx/proof-engine/tactics.rst"
+    "doc/sphinx/proofs/automatic-tactics/auto.rst";
+    "doc/sphinx/proofs/writing-proofs/rewriting.rst";
+    "doc/sphinx/proofs/writing-proofs/proof-mode.rst";
+    "doc/sphinx/proof-engine/tactics.rst";
   ]
   in
 
@@ -2021,13 +2033,11 @@ let report_omitted_prods g seen label split =
         (if first = "" then nt else first), nt, n + 1, total + 1)
     ("", "", 0, 0) !g.order in
   maybe_warn first last n;
-  (*
-  Printf.printf "\n";
+  Printf.printf "\n\n";
   NTMap.iter (fun nt _ ->
       if not (NTMap.mem nt seen || (List.mem nt included)) then
         warn "%s %s not included in .rst files\n" "Nonterminal" nt)
     !g.map;
-  *)
   if total <> 0 then
     Printf.eprintf "TOTAL %ss not included = %d\n" label total
 
@@ -2090,7 +2100,7 @@ let process_grammar args =
       print_in_order out g `MLG !g.order StringSet.empty;
       close_out out;
       finish_with_file (dir "orderedGrammar") args;
-      check_singletons g;
+(*      check_singletons g*)
 (*      print_dominated g*)
 
       let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in
@@ -2185,5 +2195,7 @@ let () =
     if !exit_code = 0 then begin
       process_grammar args
     end;
+    if !error_count > 0 then
+      Printf.eprintf "%d error(s)\n" !error_count;
     exit !exit_code
   (*with _ -> Printexc.print_backtrace stdout; exit 1*)
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 ")"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 94a6fa730b..c697043f27 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -174,10 +174,129 @@ subsequent_letter: [
 | [ first_letter | digit | "'" | unicode_id_part ]
 ]
 
-firstorder_rhs: [
-| OPT firstorder_using
-| "with" LIST1 ident
-| OPT firstorder_using "with" LIST1 ident
+ssrarg: [
+| OPT ssrfwdview OPT ssreqpat ssrdgens OPT ssrintros
+| ssrfwdview OPT ssrclear OPT ssrintros      (* SSR plugin *)
+| ssrclear OPT ssrintros      (* SSR plugin *)
+| ssrintros      (* SSR plugin *)
+]
+
+ssreqpat: [
+| ident      (* SSR plugin *)
+| "_"      (* SSR plugin *)
+| "?"      (* SSR plugin *)
+| "+"      (* SSR plugin *)
+| ssrdocc "->"      (* SSR plugin *)
+| ssrdocc "<-"      (* SSR plugin *)
+| "->"      (* SSR plugin *)
+| "<-"      (* SSR plugin *)
+]
+
+ssrapplyarg: [
+| ssrclear OPT ssrintros      (* SSR plugin *)
+| ssrintros      (* SSR plugin *)
+| OPT ssrbwdview ":" ssragen OPT ssragens OPT ssrintros      (* SSR plugin *)
+| ssrbwdview OPT ssrclear OPT ssrintros      (* SSR plugin *)
+]
+
+ssragen: [
+| OPT ( "{" LIST1 ident "}" ) term      (* SSR plugin *)
+]
+
+ssragens: [
+| "{" LIST1 ident "}" term OPT ssragens      (* SSR plugin *)
+| "{" LIST1 ident "}"      (* SSR plugin *)
+| term OPT ssragens      (* SSR plugin *)
+]
+
+ssrintros: [
+| "=>" ssripats      (* SSR plugin *)
+]
+
+ssrbwdview: [
+| "/" term      (* SSR plugin *)
+| "/" term ssrbwdview      (* SSR plugin *)
+]
+
+ssrdgens: [
+| ":" ssrgen OPT ( "/" ssrgen )      (* SSR plugin *)
+]
+
+ssrgen: [
+| cpattern LIST0 [ LIST1 ident | cpattern ]      (* SSR plugin *)
+]
+
+rewrite_item: [
+| "-" OPT mult OPT occ_or_clear OPT ssrpattern_squarep r_item      (* SSR plugin *)
+| mult OPT occ_or_clear OPT ssrpattern_squarep r_item      (* SSR plugin *)
+| "-/" term      (* SSR plugin *)
+| OPT ( OPT ( "{" LIST1 ident "}" ) ssrpattern_squarep ) r_item      (* SSR plugin *)
+| "{" LIST1 ident "}" OPT r_item      (* SSR plugin *)
+| "{" OPT ssr_occurrences "}" OPT ssrpattern_squarep r_item      (* SSR plugin *)
+]
+
+occ_or_clear: [
+| clear_switch
+| "{" ssr_occurrences "}"      (* SSR plugin *)
+]
+
+clear_switch: [
+| "{" LIST0 ident "}"
+]
+
+ssr_occurrences: [
+| [ natural | "+" | "-" ] LIST0 natural      (* SSR plugin *)
+]
+
+r_item: [
+| [ OPT "/" term | s_item ]      (* SSR plugin *)
+]
+
+ssrpattern_squarep: [
+| "[" rewrite_pattern "]"      (* SSR plugin *)
+]
+
+rewrite_pattern: [
+| OPT ( OPT ( OPT ( OPT term "in" ) term ) "in" ) term      (* SSR plugin *)
+| term "as" term "in" term      (* SSR plugin *)
+]
+
+ssr_in: [
+| "in" ssrclausehyps OPT "|-" OPT "*"      (* SSR plugin *)
+| "in" [ "*" | "*" "|-" | "|-" "*" ]      (* SSR plugin *)
+]
+
+ssrclausehyps: [
+| gen_item LIST0 ( OPT "," gen_item )      (* SSR plugin *)
+]
+
+gen_item: [
+| ssrclear      (* SSR plugin *)
+| OPT "@" ident      (* SSR plugin *)
+| "(" ident OPT ( ":=" lcpattern ) ")"      (* SSR plugin *)
+| "(@" ident ":=" lcpattern ")"      (* SSR plugin *)
+]
+
+ssrclear: [
+| "{" LIST1 ident "}"      (* SSR plugin *)
+]
+
+lcpattern: [
+| term
+]
+
+ssrsufffwd: [
+| OPT ssripats LIST0 ssrbinder ":" term OPT ( "by" ssrhintarg )      (* SSR plugin *)
+]
+
+ssrviewpos: [
+| "for" "move" "/"      (* SSR plugin *)
+| "for" "apply" "/"      (* SSR plugin *)
+| "for" "apply" "//"      (* SSR plugin *)
+]
+
+ssr_one_term_pattern: [
+| one_term      (* SSR plugin *)
 ]
 
 where: [
@@ -347,6 +466,10 @@ term_if: [
 | "if" term OPT [ OPT [ "as" name ] "return" term100 ] "then" term "else" term
 ]
 
+ssr_dpat: [
+| pattern OPT ( OPT ( "in" pattern ) "return" term100 )      (* SSR plugin *)
+]
+
 term_let: [
 | "let" name OPT ( ":" type ) ":=" term "in" term
 | "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
@@ -885,6 +1008,10 @@ command: [
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
+| "Prenex" "Implicits" LIST1 qualid      (* SSR plugin *)
+| "Print" "Hint" "View" OPT ssrviewpos      (* SSR plugin *)
+| "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) )      (* SSR plugin *)
+| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) )      (* SSR plugin *)
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
@@ -909,7 +1036,7 @@ command: [
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
 | "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name
-| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier
+| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT deprecated_number_modifier
 | "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
@@ -964,6 +1091,7 @@ command: [
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
 | "Set" setting_name OPT [ integer | string ]
 | "Unset" setting_name
+| "Import" "Prenex" "Implicits"      (* SSR plugin *)
 | "Open" "Scope" scope
 | "Close" "Scope" scope
 | "Delimit" "Scope" scope_name "with" scope_key
@@ -1117,13 +1245,11 @@ lident: [
 
 destruction_arg: [
 | natural
-| one_term OPT ( "with" bindings )
 | constr_with_bindings_arg
 ]
 
 constr_with_bindings_arg: [
-| ">" one_term OPT ( "with" bindings )
-| one_term OPT ( "with" bindings )
+| OPT ">" one_term OPT ( "with" bindings )      (* SSR plugin *)
 ]
 
 clause_dft_concl: [
@@ -1143,8 +1269,8 @@ hypident_occ: [
 
 hypident: [
 | ident
-| "(" "type" "of" ident ")"
-| "(" "value" "of" ident ")"
+| "(" "type" "of" ident ")"      (* SSR plugin *)
+| "(" "value" "of" ident ")"      (* SSR plugin *)
 ]
 
 concl_occ: [
@@ -1269,8 +1395,119 @@ field_mod: [
 | "completeness" one_term      (* ring plugin *)
 ]
 
+ssrmmod: [
+| "!"      (* SSR plugin *)
+| "?"      (* SSR plugin *)
+]
+
+mult: [
+| OPT natural ssrmmod      (* SSR plugin *)
+]
+
+ssrwlogfwd: [
+| ":" LIST0 gen_item "/" term      (* SSR plugin *)
+]
+
+ssrhintarg: [
+| "[" OPT ssrortacs "]"      (* SSR plugin *)
+| ltac_expr      (* SSR plugin *)
+]
+
+ssrortacs: [
+| OPT ltac_expr "|" OPT ssrortacs
+| ltac_expr      (* SSR plugin *)
+]
+
+ssrhint3arg: [
+| "[" OPT ssrortacs "]"      (* SSR plugin *)
+| ltac_expr3      (* SSR plugin *)
+]
+
+ssrdefbody: [
+| OPT ( ":" term ) ":=" term      (* SSR plugin *)
+]
+
+i_item: [
+| "_"      (* SSR plugin *)
+| "*"      (* SSR plugin *)
+| ">"      (* SSR plugin *)
+| ident
+| "?"      (* SSR plugin *)
+| "+"      (* SSR plugin *)
+| "++"      (* SSR plugin *)
+| s_item      (* SSR plugin *)
+| ssrdocc OPT [ "->" | "<-" ]      (* SSR plugin *)
+| "-"      (* SSR plugin *)
+| "-/="      (* SSR plugin *)
+| "-//"      (* SSR plugin *)
+| "-//="      (* SSR plugin *)
+| "-/" integer [ "/=" | "/" | "/" integer "=" ]      (* SSR plugin *)
+| ssrfwdview      (* SSR plugin *)
+| "[:" LIST0 ident "]"      (* SSR plugin *)
+| ssrblockpat      (* SSR plugin *)
+]
+
+ssrhpats_wtransp: [
+| OPT ssripats      (* SSR plugin *)
+| OPT ssripats "@" OPT ssripats      (* SSR plugin *)
+]
+
+ssripats: [
+| LIST1 i_item      (* SSR plugin *)
+]
+
+s_item: [
+| "//"      (* SSR plugin *)
+| "/="      (* SSR plugin *)
+| "//="      (* SSR plugin *)
+| "/" natural "/" natural "="      (* SSR plugin *)
+| "/" natural "/="      (* SSR plugin *)
+]
+
+ssrdocc: [
+| "{" ssr_occurrences "}"      (* SSR plugin *)
+| "{" LIST0 ident "}"      (* SSR plugin *)
+]
+
+ssrfwdview: [
+| LIST1 ( "/" one_term )      (* SSR plugin *)
+]
+
+hat: [
+| "^" ident      (* SSR plugin *)
+| "^~" ident      (* SSR plugin *)
+| "^~" natural      (* SSR plugin *)
+]
+
+ssriorpat: [
+| ssripats OPT ( [ "|" | "|-" ] ssriorpat )      (* SSR plugin *)
+]
+
+ssrblockpat: [
+| "[" hat "]"      (* SSR plugin *)
+| "[" ssriorpat "]"      (* SSR plugin *)
+| "[=" ssriorpat "]"      (* SSR plugin *)
+]
+
+ssrbinder: [
+| ssrbvar      (* SSR plugin *)
+| "(" LIST1 ssrbvar ":" term ")"      (* SSR plugin *)
+| "(" ssrbvar OPT ( ":" term ) OPT ( ":=" term ) ")"      (* SSR plugin *)
+| "of" term10      (* SSR plugin *)
+| "&" term10      (* SSR plugin *)
+]
+
+ssrbvar: [
+| ident      (* SSR plugin *)
+| "_"      (* SSR plugin *)
+]
+
+ssrhavefwd: [
+| ":" term OPT ( "by" ssrhintarg )      (* SSR plugin *)
+| ":" term ":=" OPT term      (* SSR plugin *)
+]
+
 deprecated_number_modifier: [
-|
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
@@ -1403,11 +1640,14 @@ simple_tactic: [
 | "infoH" ltac_expr3
 | "abstract" ltac_expr2 OPT ( "using" ident )
 | "only" selector ":" ltac_expr3
+| "do" "[" ssrortacs "]" OPT ssr_in      (* SSR plugin *)
+| "do" OPT int_or_var ssrmmod [ ltac_expr3 | "[" ssrortacs "]"      (* SSR plugin *) ] OPT ssr_in      (* SSR plugin *)
 | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 [ ident | string | natural ]
 | [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ]
+| ltac_expr ssrintros      (* SSR plugin *)
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
@@ -1595,7 +1835,7 @@ simple_tactic: [
 | "rtauto"
 | "congruence" OPT natural OPT ( "with" LIST1 one_term )
 | "f_equal"
-| "firstorder" OPT ltac_expr firstorder_rhs
+| "firstorder" OPT ltac_expr OPT ( "using" LIST1 qualid SEP "," ) OPT ( "with" LIST1 ident )
 | "gintuition" OPT ltac_expr
 | "functional" "inversion" [ ident | natural ] OPT qualid      (* funind plugin *)
 | "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern )      (* funind plugin *)
@@ -1622,12 +1862,47 @@ simple_tactic: [
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
+| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
+| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
+| "by" ssrhintarg      (* SSR plugin *)
+| "clear" natural      (* SSR plugin *)
+| "move" OPT ( OPT ssrarg [ "->" | "<-" ] )      (* SSR plugin *)
+| "move" ssrarg OPT ssr_in      (* SSR plugin *)
+| "case" OPT ( ssrarg OPT ssr_in )      (* SSR plugin *)
+| "elim" OPT ( ssrarg OPT ssr_in )      (* SSR plugin *)
+| "apply" OPT ssrapplyarg      (* SSR plugin *)
+| "exact" [ ":" ssragen OPT ssragens | ssrbwdview OPT ssrclear | ssrclear ]      (* SSR plugin *)
+| "exact"      (* SSR plugin *)
+| "exact" "<:" term      (* SSR plugin *)
+| "congr" OPT natural one_term OPT ssrdgens      (* SSR plugin *)
+| "ssrinstancesofruleL2R" term      (* SSR plugin *)
+| "ssrinstancesofruleR2L" term      (* SSR plugin *)
+| "rewrite" LIST1 rewrite_item OPT ssr_in      (* SSR plugin *)
+| "unlock" LIST0 ( OPT ( "{" ssr_occurrences "}" ) term ) OPT ssr_in      (* SSR plugin *)
+| "pose" "fix" ssrbvar LIST0 ssrbinder OPT ( "{" "struct" ident "}" ) ssrdefbody      (* SSR plugin *)
+| "pose" "cofix" ssrbvar LIST0 ssrbinder ssrdefbody      (* SSR plugin *)
+| "pose" ident LIST0 ssrbinder ssrdefbody      (* SSR plugin *)
+| "set" ident OPT ( ":" term ) ":=" [ "{" ssr_occurrences "}" cpattern | lcpattern ] OPT ssr_in      (* SSR plugin *)
+| "abstract" ssrdgens      (* SSR plugin *)
+| "have" ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd      (* SSR plugin *)
+| "have" [ "suff" | "suffices" ] OPT ssripats ssrhavefwd      (* SSR plugin *)
+| [ "suff" | "suffices" ] OPT ( "have" OPT ssripats ) ssrhavefwd      (* SSR plugin *)
+| [ "suff" | "suffices" ] ssrsufffwd      (* SSR plugin *)
+| [ "wlog" | "without loss" ] OPT [ "suff" | "suffices" ] OPT ssripats ssrwlogfwd OPT ( "by" ssrhintarg )      (* SSR plugin *)
+| [ "gen" | "generally" ] "have" OPT ssrclear OPT ( [ ident | "_" ] "," ) OPT ssripats ssrwlogfwd OPT ( "by" ssrhintarg )      (* SSR plugin *)
+| "under" rewrite_item OPT ssrintros OPT ( "do" ssrhint3arg )      (* SSR plugin *)
+| "ssrinstancesoftpat" ssr_one_term_pattern      (* SSR plugin *)
+| ltac_expr ";" "first" ssr_first_else      (* SSR plugin *)
+| ltac_expr ";" "first" ssrseqarg      (* SSR plugin *)
+| ltac_expr ";" "last" ssrseqarg      (* SSR plugin *)
 | match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
 | match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
 | "classical_left"
 | "classical_right"
 | "contradict" ident
+| "dintuition" OPT ltac_expr
 | "discrR"
+| "dtauto"
 | "easy"
 | "exfalso"
 | "inversion_sigma"
@@ -1635,6 +1910,7 @@ simple_tactic: [
 | "lra"
 | "nia"
 | "nra"
+| "over"      (* SSR plugin *)
 | "split_Rabs"
 | "split_Rmult"
 | "tauto"
@@ -1685,20 +1961,25 @@ as_name: [
 | "as" ident
 ]
 
+oriented_rewriter: [
+| OPT [ "->" | "<-" ] rewriter
+]
+
 rewriter: [
 | OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
 ]
 
-oriented_rewriter: [
-| OPT [ "->" | "<-" ] rewriter
+induction_clause_list: [
+| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause
 ]
 
 induction_clause: [
 | destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause
 ]
 
-induction_clause_list: [
-| LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause
+opt_clause: [
+| "in" in_clause
+| "at" occs_nums
 ]
 
 auto_using: [
@@ -2133,11 +2414,6 @@ clause_dft_all: [
 | "in" in_clause
 ]
 
-opt_clause: [
-| "in" in_clause
-| "at" occs_nums
-]
-
 in_hyp_as: [
 | "in" ident OPT as_ipat
 ]
@@ -2165,12 +2441,6 @@ conversion: [
 | one_term "at" occs_nums "with" one_term
 ]
 
-firstorder_using: [
-| "using" qualid
-| "using" qualid "," LIST1 qualid SEP ","
-| "using" qualid qualid LIST0 qualid
-]
-
 func_scheme_def: [
 | ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]
@@ -2276,6 +2546,34 @@ tactic_atom: [
 | "()"
 ]
 
+ssrseqarg: [
+| ssrseqidx "[" ssrortacs "]" OPT ssrorelse      (* SSR plugin *)
+| OPT ssrseqidx ssrswap      (* SSR plugin *)
+| ltac_expr3      (* SSR plugin *)
+]
+
+ssrseqidx: [
+| ident      (* SSR plugin *)
+| natural      (* SSR plugin *)
+]
+
+ssrorelse: [
+| "||" ltac_expr2      (* SSR plugin *)
+]
+
+ssrswap: [
+| "first"      (* SSR plugin *)
+| "last"      (* SSR plugin *)
+]
+
+ssr_first_else: [
+| ssr_first OPT ssrorelse      (* SSR plugin *)
+]
+
+ssr_first: [
+| "[" LIST0 ltac_expr SEP "|" "]" LIST0 ssrintros      (* SSR plugin *)
+]
+
 let_clause: [
 | name ":=" ltac_expr
 | ident LIST1 name ":=" ltac_expr