Topics:
- Setting of mutable Ltac definitions from tactic (17 messages, latest: Mar 08 2023 at 09:30)
- issue prioritization (4 messages, latest: Mar 03 2023 at 08:32)
- with_strategy and abstract (5 messages, latest: Feb 22 2023 at 13:28)
- Ltac2 library, typeclasses (28 messages, latest: Dec 03 2022 at 20:56)
- pi quantifier (36 messages, latest: Nov 23 2022 at 11:05)
- Replace the type of the goal (6 messages, latest: Nov 17 2022 at 10:07)
- Roll-your-own apply, rewrite (1 message, latest: Nov 06 2022 at 23:27)
- Ltac2 AST (19 messages, latest: Oct 25 2022 at 18:52)
- ✔ `constr:(...)` printing (4 messages, latest: Oct 23 2022 at 09:52)
- matches_subterm (14 messages, latest: Oct 21 2022 at 08:47)
- Debugging, Std.set, patterns (8 messages, latest: Oct 20 2022 at 00:08)
- ✔ matches_subterm (11 messages, latest: Oct 19 2022 at 12:14)
- Ltac2 learning resources (5 messages, latest: Oct 11 2022 at 21:16)
- evar normalization (6 messages, latest: Oct 06 2022 at 15:41)
- Alternatives to `Control.new_goal` (1 message, latest: Oct 06 2022 at 11:14)
- Performance (2 messages, latest: Oct 03 2022 at 14:18)
- Performance worse than Ltac1 (76 messages, latest: Oct 01 2022 at 08:41)
- Locating evars (1 message, latest: Sep 28 2022 at 10:45)
- ✔ Performance of antiquotation (8 messages, latest: Sep 26 2022 at 15:26)
- Constr mapping (1 message, latest: Sep 26 2022 at 05:07)
- `Not_found` anomalies with `Constr.Unsafe` (13 messages, latest: Sep 24 2022 at 10:24)
- ✔ Why does `Control.refine` take a thunk? (5 messages, latest: Sep 23 2022 at 10:48)
- Discourse question (1 message, latest: Sep 19 2022 at 07:06)
- Ltac1.of_constr only works after `idtac x` (5 messages, latest: Sep 16 2022 at 15:48)
- Query the strategy of a symbol in Ltac2 (9 messages, latest: Sep 14 2022 at 19:21)
- Ltac2 Set locality? (1 message, latest: Aug 29 2022 at 06:13)
- performance diffing Ltac2 vs Ltac (1 message, latest: Aug 29 2022 at 03:42)
- liftn (3 messages, latest: Aug 28 2022 at 15:44)
- printf %a (1 message, latest: Aug 27 2022 at 13:21)
- incremental porting of Ltac1 code? (1 message, latest: Aug 27 2022 at 06:32)
- `Ltac2 Set` on non-mutable Ltac2 definitions (2 messages, latest: Aug 26 2022 at 08:29)
- Exposing Ltac2 variadic notations in Ltac1 (22 messages, latest: Aug 19 2022 at 07:46)
- writing efficient variant of `clear` (18 messages, latest: Jul 23 2022 at 17:22)
- Internal representation of lists (9 messages, latest: Jul 19 2022 at 20:57)
- How to count goals? (7 messages, latest: Jun 09 2022 at 19:26)
- Entry for Ltac2 Tactic Notation (2 messages, latest: Jun 08 2022 at 12:46)
- Resources to learn Ltac/Ltac2 (3 messages, latest: May 31 2022 at 13:02)
- ✔ use Gallina string with ltac's fresh (14 messages, latest: May 16 2022 at 08:43)
- stream events (2 messages, latest: Apr 18 2022 at 09:00)
- Ltac2 quiz on `ltac2` (5 messages, latest: Apr 16 2022 at 21:56)
- Go back and forth issue in VsCoq (3 messages, latest: Mar 08 2022 at 17:56)
- apply with implicit arguments (10 messages, latest: Feb 16 2022 at 10:19)
- Goal selectors (5 messages, latest: Feb 15 2022 at 18:01)
- Ltac2 integer operations (4 messages, latest: Feb 07 2022 at 13:28)
- Notation for refine (39 messages, latest: Feb 04 2022 at 15:22)
- Definition of list (4 messages, latest: Feb 04 2022 at 13:32)
- Notation scopes for Printf (24 messages, latest: Feb 04 2022 at 08:11)
- Creating a fresh ident (29 messages, latest: Feb 03 2022 at 17:37)
- Introducing in the context (71 messages, latest: Feb 03 2022 at 16:15)
- Issues with try-catch via Control.plus (8 messages, latest: Feb 02 2022 at 16:00)
- Evar in Ltac2 (7 messages, latest: Feb 02 2022 at 09:16)
- Constr binders (5 messages, latest: Feb 01 2022 at 17:38)
- Error in Qed after using Ltac2 Eval in proof context (16 messages, latest: Jan 28 2022 at 20:49)
- Ltac2 warfare (7 messages, latest: Jan 06 2022 at 17:28)
- Ltac2 in Notations (9 messages, latest: Dec 16 2021 at 19:20)
- Goal number (2 messages, latest: Nov 26 2021 at 01:45)
- Term syntax for variable assignments (79 messages, latest: Nov 11 2021 at 14:16)
- Hash table (36 messages, latest: Nov 11 2021 at 11:58)
- Ltac2 `or` semantic (1 message, latest: Oct 28 2021 at 13:32)
- Why Ltac2 cannot obsolete Ltac1 yet (30 messages, latest: Oct 02 2021 at 15:32)
- ✔ What to do instead of semicolons? (45 messages, latest: Oct 02 2021 at 12:36)
- Postfix Ltac2 notation (3 messages, latest: Jun 29 2021 at 07:24)
- Ltac1 - Ltac2 interaction (4 messages, latest: Jun 29 2021 at 07:21)
- simple apply (1 message, latest: Mar 27 2021 at 09:42)
- change term1 with term2 (30 messages, latest: Mar 26 2021 at 09:56)
- How can I control the depth of "Message.of_constr"? (5 messages, latest: Mar 21 2021 at 19:59)
- Gallina globals hide locals in Ltac2 terms (28 messages, latest: Mar 20 2021 at 18:54)
- Calling ring_simplify with a list of terms (7 messages, latest: Mar 19 2021 at 13:43)
- Using ids with context match (15 messages, latest: Mar 19 2021 at 09:25)
- Precedence of ";" with "by" (18 messages, latest: Mar 12 2021 at 18:12)
- Issues with calling Ltac1 tactic notations (5 messages, latest: Mar 10 2021 at 09:32)
- pose proof / issues with ltac2 in assert (6 messages, latest: Mar 06 2021 at 14:24)
- How to catch an exception (5 messages, latest: Mar 05 2021 at 13:58)
- Continue the $ notation discussion (2 messages, latest: Feb 26 2021 at 11:10)
Last updated: Mar 25 2023 at 07:28 UTC