diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-12-30 11:48:37 -0800 |
| commit | e02120ed6580733db2276f0c11b4f432ea670ee3 (patch) | |
| tree | 19c809eeea61fe131e4b4b15bc0bc72c617cce53 /doc/tools/docgram/common.edit_mlg | |
| parent | 532cbed036c48ed2c77528b79fc947c4bc7e1c10 (diff) | |
Convert rewriting and proof-mode chapters to prodn
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 17 |
1 files changed, 15 insertions, 2 deletions
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: [ |