diff options
| author | coqbot-app[bot] | 2020-11-10 21:30:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 21:30:52 +0000 |
| commit | 417e8c513e4372bcd622603912cfb2d9f1069619 (patch) | |
| tree | c999417af80830af45f685751337bf3124652b92 /doc/sphinx/proof-engine | |
| parent | fa6c67d721d4178d6b82571feef33c887aef5ba2 (diff) | |
| parent | da9fd81c887024e991467d4dd586661c4ca01022 (diff) | |
Merge PR #13315: Convert logic chapter to prodn
Reviewed-by: Zimmi48
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 | 10 |
2 files changed, 9 insertions, 9 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 b912bcbdf8..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 @@ -1633,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_oriented_rewriter ltac2_rewriter .. prodn:: - ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter + ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics |