diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-10 10:21:18 -0800 |
| commit | da9fd81c887024e991467d4dd586661c4ca01022 (patch) | |
| tree | 001e9bff33c8d759a8cb79351e2ef36a9839e0c8 /doc/sphinx/proof-engine | |
| parent | 7d8389d012aa8dbdeb7b82217087f1b7dfb2b24e (diff) | |
Convert logic.rst to prodn
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index e1f57c9bea..6464f085b8 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -60,7 +60,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`. ltac_expr3 ::= @l3_tactic | @ltac_expr2 ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic } - | @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } + | @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } | @l2_tactic | @ltac_expr1 ltac_expr1 ::= @tactic_value @@ -729,7 +729,7 @@ First tactic to make progress: || Yet another way of branching without backtracking is the following structure: -.. tacn:: @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } +.. tacn:: @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } :name: || (first tactic making progress) :n:`@ltac_expr1 || @ltac_expr2` is @@ -1353,8 +1353,8 @@ Pattern matching on goals and hypotheses: match goal .. insertprodn goal_pattern match_hyp .. prodn:: - goal_pattern ::= {*, @match_hyp } |- @match_pattern - | [ {*, @match_hyp } |- @match_pattern ] + goal_pattern ::= {*, @match_hyp } %|- @match_pattern + | [ {*, @match_hyp } %|- @match_pattern ] | _ match_hyp ::= @name : @match_pattern | @name := @match_pattern diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 81c497d60a..a46f4fb894 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -562,7 +562,7 @@ Built-in quotations | ltac1 : ( @ltac1_expr_in_env ) | ltac1val : ( @ltac1_expr_in_env ) ltac1_expr_in_env ::= @ltac_expr - | {* @ident } |- @ltac_expr + | {* @ident } %|- @ltac_expr The current implementation recognizes the following built-in quotations: @@ -978,7 +978,7 @@ Match over goals .. prodn:: goal_match_list ::= {? %| } {+| @gmatch_rule } gmatch_rule ::= @gmatch_pattern => @ltac2_expr - gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } |- @ltac2_match_pattern ] + gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } %|- @ltac2_match_pattern ] gmatch_hyp_pattern ::= @name : @ltac2_match_pattern Matches over goals, similar to Ltac1 :tacn:`match goal`. @@ -1602,8 +1602,8 @@ Here is the syntax for the :n:`q_*` nonterminals: ltac2_clause ::= in @ltac2_in_clause | at @ltac2_occs_nums ltac2_in_clause ::= * {? @ltac2_occs } - | * |- {? @ltac2_concl_occ } - | {*, @ltac2_hypident_occ } {? |- {? @ltac2_concl_occ } } + | * %|- {? @ltac2_concl_occ } + | {*, @ltac2_hypident_occ } {? %|- {? @ltac2_concl_occ } } .. insertprodn q_occurrences ltac2_hypident |