From e02120ed6580733db2276f0c11b4f432ea670ee3 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert rewriting and proof-mode chapters to prodn

---
 doc/tools/docgram/common.edit_mlg | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

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: [
-- 
cgit v1.2.3