Merge PR #13470: Convert rewriting and proof-mode chapters to prodn

Reviewed-by: Zimmi48
Ack-by: JasonGross

4 files changed, 30 insertions, 28 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 35243b5d7d..fa739e97bc 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -345,7 +345,7 @@ class VernacVariantObject(VernacObject):
        .. cmd:: Axiom @ident : @term.
 
           This command links :token:`term` to the name :token:`term` as its specification in
-          the global context. The fact asserted by :token:`term` is thus assumed as a
+          the global environment. The fact asserted by :token:`term` is thus assumed as a
           postulate.
 
           .. cmdv:: Parameter @ident : @term.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 75b3260166..f267cdb697 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1003,7 +1003,7 @@ simple_tactic: [
 | DELETE "replace" uconstr clause
 | "replace" orient uconstr clause
 | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac
-| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac )
+| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences ) by_arg_tac
 | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac
 | DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac
 | DELETE "rewrite" "*" orient uconstr by_arg_tac
@@ -1814,6 +1814,7 @@ ltac_defined_tactics: [
 | "lia"
 | "lra"
 | "nia"
+| "now_show" constr
 | "nra"
 | "over"  TAG SSR
 | "split_Rabs"
@@ -2373,7 +2374,7 @@ ssrapplyarg: [
 ]
 
 constr_with_bindings_arg: [
-| EDIT ADD_OPT ">" constr_with_bindings      TAG SSR
+| EDIT ADD_OPT ">" constr_with_bindings
 ]
 
 destruction_arg: [
@@ -2469,6 +2470,15 @@ variance_identref: [
 | EDIT ADD_OPT variance identref
 ]
 
+conversion: [
+| DELETE constr
+| DELETE constr "with" constr
+| PRINT
+| REPLACE constr "at" occs_nums "with" constr
+| WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr
+| PRINT
+]
+
 SPLICE: [
 | clause
 | noedit_mode
@@ -2694,6 +2704,8 @@ SPLICE: [
 | cumul_ident_decl
 | variance
 | variance_identref
+| rewriter
+| conversion
 ] (* end SPLICE *)
 
 RENAME: [
@@ -2751,6 +2763,7 @@ RENAME: [
 | pattern_occ pattern_occs
 | hypident_occ hyp_occs
 | concl_occ concl_occs
+| constr_with_bindings_arg one_term_with_bindings
 ]
 
 simple_tactic: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index dd7990368e..a1c1d87763 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1726,8 +1726,6 @@ 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/proofs/writing-proofs/rewriting.rst";
-    "doc/sphinx/proofs/writing-proofs/proof-mode.rst";
     "doc/sphinx/proof-engine/tactics.rst";
   ]
   in
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index d950b32160..72e101446c 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1247,11 +1247,7 @@ lident: [
 
 destruction_arg: [
 | natural
-| constr_with_bindings_arg
-]
-
-constr_with_bindings_arg: [
-| OPT ">" one_term OPT ( "with" bindings )      (* SSR plugin *)
+| one_term_with_bindings
 ]
 
 occurrences: [
@@ -1691,7 +1687,7 @@ simple_tactic: [
 | "absurd" one_term
 | "contradiction" OPT ( one_term OPT ( "with" bindings ) )
 | "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr )
-| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) )
+| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs ) OPT ( "by" ltac_expr3 )
 | "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 )
 | "refine" one_term
 | "simple" "refine" one_term
@@ -1783,12 +1779,12 @@ simple_tactic: [
 | "eintros" LIST0 intropattern
 | "decide" "equality"
 | "compare" one_term one_term
-| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
-| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
-| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
-| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as
-| "elim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) )
-| "eelim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) )
+| "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
+| "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
+| "simple" "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
+| "simple" "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as
+| "elim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) )
+| "eelim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
 | "fix" ident natural OPT ( "with" LIST1 fixdecl )
@@ -1842,8 +1838,8 @@ simple_tactic: [
 | "unfold" LIST1 reference_occs SEP "," OPT occurrences
 | "fold" LIST1 one_term OPT occurrences
 | "pattern" LIST1 pattern_occs SEP "," OPT occurrences
-| "change" conversion OPT occurrences
-| "change_no_check" conversion OPT occurrences
+| "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
+| "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
 | "btauto"
 | "rtauto"
 | "congruence" OPT natural OPT ( "with" LIST1 one_term )
@@ -1922,6 +1918,7 @@ simple_tactic: [
 | "lia"
 | "lra"
 | "nia"
+| "now_show" one_term
 | "nra"
 | "over"      (* SSR plugin *)
 | "split_Rabs"
@@ -1977,11 +1974,11 @@ as_name: [
 ]
 
 oriented_rewriter: [
-| OPT [ "->" | "<-" ] rewriter
+| OPT [ "->" | "<-" ] OPT natural OPT [ "?" | "!" ] one_term_with_bindings
 ]
 
-rewriter: [
-| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
+one_term_with_bindings: [
+| OPT ">" one_term OPT ( "with" bindings )
 ]
 
 induction_clause_list: [
@@ -2454,12 +2451,6 @@ cofixdecl: [
 | "(" ident LIST0 simple_binder ":" term ")"
 ]
 
-conversion: [
-| one_term
-| one_term "with" one_term
-| one_term "at" occs_nums "with" one_term
-]
-
 func_scheme_def: [
 | ident ":=" "Induction" "for" qualid "Sort" sort_family      (* funind plugin *)
 ]