From 502d1e95f3f9ffb5c0f894513929eec4fe3c7c37 Mon Sep 17 00:00:00 2001 From: Ambroise Date: Fri, 14 Aug 2026 07:11:07 +0200 Subject: [PATCH 1/2] Fix syntax and parsing examples in tutorial_ltac2 --- src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index a6393d9..5c9044e 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -258,8 +258,8 @@ Qed. (** In Ltac2, this is now written with the syntax [tac1 > [tac21 | tac22]] in order to avoid confusion between chaining tactics and dispatching. The latter is asymetric and does not compose opposite to [;]. - Moreover, [tac1; tac2; [tac31 | tac32]] - is now parsed as [tac1; (tac2; [tac31 | tac32])] as Ltac2 no longer + Moreover, [tac1; tac2 > [tac31 | tac32]] + is now parsed as [tac1; (tac2 > [tac31 | tac32])] as Ltac2 no longer automatically delays tactic execution. Consequently, if [tac1] generates multiple goals, the dispatcher will @@ -947,7 +947,7 @@ Ltac2 rec my_first0 tacs := (** To write a notation for it, we write: - - ["my_first"] and ["["] / ["]"] are literal keywords that the parser matches + - ["my_first"] and "[" / "]" are literal keywords that the parser matches verbatim; so that [my_first [...]] is unambiguous - [tacs] is the name bound in the body to the parsed argument From 1d23ca14bad04d687a4500e5915888d4b091ea98 Mon Sep 17 00:00:00 2001 From: Ambroise Date: Fri, 14 Aug 2026 07:15:25 +0200 Subject: [PATCH 2/2] Update tutorial_ltac2_for_ltac1_users.v --- src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 5c9044e..d10f141 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -258,8 +258,8 @@ Qed. (** In Ltac2, this is now written with the syntax [tac1 > [tac21 | tac22]] in order to avoid confusion between chaining tactics and dispatching. The latter is asymetric and does not compose opposite to [;]. - Moreover, [tac1; tac2 > [tac31 | tac32]] - is now parsed as [tac1; (tac2 > [tac31 | tac32])] as Ltac2 no longer + Moreover, [tac1; tac2 > [tac31 | tac32]] + is now parsed as [tac1; (tac2 > [tac31 | tac32])] as Ltac2 no longer automatically delays tactic execution. Consequently, if [tac1] generates multiple goals, the dispatcher will