diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 40 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 52 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 53 |
3 files changed, 77 insertions, 68 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 816acba4c1..4080eaae08 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -815,7 +815,10 @@ 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 +(* | EDIT "do" ADD_OPT nat_or_var ssrmmod ssrdotac ssrclauses TAG SSR *) +| DELETE "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| DELETE "do" ssrortacarg ssrclauses (* SSR plugin *) +| DELETE "do" nat_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) | MOVEALLBUT ltac_builtins | l3_tactic | ltac_expr2 @@ -917,13 +920,13 @@ simple_tactic: [ | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) | DELETE "constructor" -| DELETE "constructor" int_or_var -| REPLACE "constructor" int_or_var "with" bindings -| WITH "constructor" OPT int_or_var OPT ( "with" bindings ) +| DELETE "constructor" nat_or_var +| REPLACE "constructor" nat_or_var "with" bindings +| WITH "constructor" OPT nat_or_var OPT ( "with" bindings ) | DELETE "econstructor" -| DELETE "econstructor" int_or_var -| REPLACE "econstructor" int_or_var "with" bindings -| WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| DELETE "econstructor" nat_or_var +| REPLACE "econstructor" nat_or_var "with" bindings +| WITH "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) ) | DELETE "dependent" "rewrite" orient constr | REPLACE "dependent" "rewrite" orient constr "in" hyp | WITH "dependent" "rewrite" orient constr OPT ( "in" hyp ) @@ -1042,12 +1045,12 @@ simple_tactic: [ | DELETE "finish_timing" OPT string | REPLACE "finish_timing" "(" string ")" OPT string | WITH "finish_timing" OPT ( "(" string ")" ) OPT string -| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr -| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr +| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr +| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" nat_or_var ) "in" constr | DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr -| EDIT "psatz_R" ADD_OPT int_or_var tactic -| EDIT "psatz_Q" ADD_OPT int_or_var tactic -| EDIT "psatz_Z" ADD_OPT int_or_var tactic +| EDIT "psatz_R" ADD_OPT nat_or_var tactic +| EDIT "psatz_Q" ADD_OPT nat_or_var tactic +| EDIT "psatz_Z" ADD_OPT nat_or_var tactic | REPLACE "subst" LIST1 hyp | WITH "subst" LIST0 hyp | DELETE "subst" @@ -1064,11 +1067,11 @@ simple_tactic: [ | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident | WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident ) -| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) -| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident -| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var -| DELETE "typeclasses" "eauto" OPT int_or_var +| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 preident ) +| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident +| DELETE "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident +| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var +| DELETE "typeclasses" "eauto" OPT nat_or_var (* 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 ) @@ -1789,7 +1792,7 @@ tactic_notation_tactics: [ | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) | "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 +| "psatz" constr OPT nat_or_var | "ring" OPT ( "[" LIST1 constr "]" ) | "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) ] @@ -2536,7 +2539,6 @@ SPLICE: [ | by_arg_tac | by_tactic | quantified_hypothesis -| nat_or_var | in_hyp_list | rename | export_token diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 03a20d621b..d01f66c6d7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1420,6 +1420,7 @@ syntax_modifiers: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "binder" @@ -1440,6 +1441,7 @@ at_level_opt: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] @@ -1479,11 +1481,11 @@ simple_tactic: [ | "right" "with" bindings | "eright" "with" bindings | "constructor" -| "constructor" int_or_var -| "constructor" int_or_var "with" bindings +| "constructor" nat_or_var +| "constructor" nat_or_var "with" bindings | "econstructor" -| "econstructor" int_or_var -| "econstructor" int_or_var "with" bindings +| "econstructor" nat_or_var +| "econstructor" nat_or_var "with" bindings | "specialize" constr_with_bindings | "specialize" constr_with_bindings "as" simple_intropattern | "symmetry" @@ -1582,9 +1584,9 @@ simple_tactic: [ | "generalize_eqs_vars" hyp | "dependent" "generalize_eqs_vars" hyp | "specialize_eqs" hyp -| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr | "hresolve_core" "(" ident ":=" constr ")" "in" constr -| "hget_evar" int_or_var +| "hget_evar" nat_or_var | "destauto" | "destauto" "in" hyp | "transparent_abstract" tactic3 @@ -1617,25 +1619,25 @@ simple_tactic: [ | "trivial" auto_using hintbases | "info_trivial" auto_using hintbases | "debug" "trivial" auto_using hintbases -| "auto" OPT int_or_var auto_using hintbases -| "info_auto" OPT int_or_var auto_using hintbases -| "debug" "auto" OPT int_or_var auto_using hintbases -| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "new" "auto" OPT int_or_var auto_using hintbases -| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "dfs" "eauto" OPT int_or_var auto_using hintbases -| "bfs" "eauto" OPT int_or_var auto_using hintbases +| "auto" OPT nat_or_var auto_using hintbases +| "info_auto" OPT nat_or_var auto_using hintbases +| "debug" "auto" OPT nat_or_var auto_using hintbases +| "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "new" "auto" OPT nat_or_var auto_using hintbases +| "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "dfs" "eauto" OPT nat_or_var auto_using hintbases +| "bfs" "eauto" OPT nat_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases | "unify" constr constr | "unify" constr constr "with" preident | "convert_concl_no_check" constr -| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident -| "typeclasses" "eauto" "bfs" OPT int_or_var -| "typeclasses" "eauto" OPT int_or_var +| "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident +| "typeclasses" "eauto" "bfs" OPT nat_or_var +| "typeclasses" "eauto" OPT nat_or_var | "head_of_constr" ident constr | "not_evar" constr | "is_ground" constr @@ -1734,7 +1736,7 @@ simple_tactic: [ | "restart_timer" OPT string | "finish_timing" OPT string | "finish_timing" "(" string ")" OPT string -| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" nat_or_var tactic (* micromega plugin *) | "psatz_Z" tactic (* micromega plugin *) | "xlia" tactic (* micromega plugin *) | "xnlia" tactic (* micromega plugin *) @@ -1745,9 +1747,9 @@ simple_tactic: [ | "sos_R" tactic (* micromega plugin *) | "lra_Q" tactic (* micromega plugin *) | "lra_R" tactic (* micromega plugin *) -| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" nat_or_var tactic (* micromega plugin *) | "psatz_R" tactic (* micromega plugin *) -| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" nat_or_var tactic (* micromega plugin *) | "psatz_Q" tactic (* micromega plugin *) | "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) @@ -2022,8 +2024,8 @@ ltac_expr4: [ ltac_expr3: [ | "try" ltac_expr3 -| "do" int_or_var ltac_expr3 -| "timeout" int_or_var ltac_expr3 +| "do" nat_or_var ltac_expr3 +| "timeout" nat_or_var ltac_expr3 | "time" OPT string ltac_expr3 | "repeat" ltac_expr3 | "progress" ltac_expr3 @@ -2036,7 +2038,7 @@ ltac_expr3: [ | ltac_expr2 | "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) | "do" ssrortacarg ssrclauses (* SSR plugin *) -| "do" int_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "do" nat_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) | "abstract" ssrdgens (* SSR plugin *) ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0209cf762a..f62dd8f731 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -652,8 +652,8 @@ ref_or_pattern_occ: [ ] occs_nums: [ -| LIST1 [ natural | ident ] -| "-" LIST1 [ natural | ident ] +| LIST1 nat_or_var +| "-" LIST1 nat_or_var ] int_or_var: [ @@ -661,6 +661,11 @@ int_or_var: [ | ident ] +nat_or_var: [ +| natural +| ident +] + unfold_occ: [ | reference OPT ( "at" occs_nums ) ] @@ -1574,6 +1579,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1586,6 +1592,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] @@ -1620,8 +1627,8 @@ simple_tactic: [ | "eleft" OPT ( "with" bindings ) | "right" OPT ( "with" bindings ) | "eright" OPT ( "with" bindings ) -| "constructor" OPT int_or_var OPT ( "with" bindings ) -| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| "constructor" OPT nat_or_var OPT ( "with" bindings ) +| "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) ) | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern ) | "symmetry" OPT ( "in" in_clause ) | "split" OPT ( "with" bindings ) @@ -1648,8 +1655,8 @@ simple_tactic: [ | bullet | "}" | "try" ltac_expr3 -| "do" int_or_var ltac_expr3 -| "timeout" int_or_var ltac_expr3 +| "do" nat_or_var ltac_expr3 +| "timeout" nat_or_var ltac_expr3 | "time" OPT string ltac_expr3 | "repeat" ltac_expr3 | "progress" ltac_expr3 @@ -1658,8 +1665,6 @@ 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 "|" "]" @@ -1718,8 +1723,8 @@ simple_tactic: [ | "generalize_eqs_vars" ident | "dependent" "generalize_eqs_vars" ident | "specialize_eqs" ident -| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term -| "hget_evar" int_or_var +| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" nat_or_var ) "in" one_term +| "hget_evar" nat_or_var | "destauto" OPT ( "in" ident ) | "transparent_abstract" ltac_expr3 OPT ( "using" ident ) | "constr_eq" one_term one_term @@ -1756,20 +1761,20 @@ simple_tactic: [ | "trivial" OPT auto_using OPT hintbases | "info_trivial" OPT auto_using OPT hintbases | "debug" "trivial" OPT auto_using OPT hintbases -| "auto" OPT int_or_var OPT auto_using OPT hintbases -| "info_auto" OPT int_or_var OPT auto_using OPT hintbases -| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases -| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases -| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases -| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "info_auto" OPT nat_or_var OPT auto_using OPT hintbases +| "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) | "convert_concl_no_check" one_term -| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 ident ) +| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident ) | "head_of_constr" ident one_term | "not_evar" one_term | "is_ground" one_term @@ -1859,7 +1864,7 @@ simple_tactic: [ | "functional" "inversion" [ ident | natural ] OPT qualid (* funind plugin *) | "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) | "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) -| "psatz_Z" OPT int_or_var ltac_expr +| "psatz_Z" OPT nat_or_var ltac_expr | "xlia" ltac_expr (* micromega plugin *) | "xnlia" ltac_expr (* micromega plugin *) | "xnra" ltac_expr (* micromega plugin *) @@ -1869,8 +1874,8 @@ simple_tactic: [ | "sos_R" ltac_expr (* micromega plugin *) | "lra_Q" ltac_expr (* micromega plugin *) | "lra_R" ltac_expr (* micromega plugin *) -| "psatz_R" OPT int_or_var ltac_expr -| "psatz_Q" OPT int_or_var ltac_expr +| "psatz_R" OPT nat_or_var ltac_expr +| "psatz_Q" OPT nat_or_var ltac_expr | "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) @@ -1942,7 +1947,7 @@ simple_tactic: [ | "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term ) -| "psatz" one_term OPT int_or_var +| "psatz" one_term OPT nat_or_var | "ring" OPT ( "[" LIST1 one_term "]" ) | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) | "match" ltac2_expr5 "with" OPT ltac2_branches "end" |