Topics:
- `exact` typechecking changes in 8.20 (9 messages, latest: Oct 10 2024 at 10:20)
- Differentiating terms with and without body (5 messages, latest: Oct 07 2024 at 11:25)
- ✔ Extend the global environment (11 messages, latest: Sep 25 2024 at 12:31)
- Understanding backtracking exceptions (6 messages, latest: Sep 25 2024 at 08:47)
- Typechecking open terms (5 messages, latest: Sep 24 2024 at 13:53)
- Building open terms (33 messages, latest: Sep 24 2024 at 11:52)
- Find a global reference in the environment (8 messages, latest: Sep 23 2024 at 11:25)
- Antiquotation for an ident (2 messages, latest: Sep 03 2024 at 12:56)
- Examples for documentation (28 messages, latest: Aug 26 2024 at 15:46)
- Matching subexpression of the goal (4 messages, latest: Jul 26 2024 at 12:26)
- ✔ Create a fresh evar using Ltac2 (6 messages, latest: Jul 11 2024 at 12:12)
- Create a fresh evar using Ltac2 (7 messages, latest: Jul 11 2024 at 11:55)
- adding error location to `Message.of_exn` (3 messages, latest: Jun 24 2024 at 22:17)
- Control.new_goal leaving goal shelved (8 messages, latest: Jun 04 2024 at 07:17)
- Constr.in_context perf issues (15 messages, latest: May 30 2024 at 14:30)
- issue prioritization (26 messages, latest: May 28 2024 at 11:44)
- thunking and `thaw` (27 messages, latest: Apr 24 2024 at 11:39)
- Ltac2 `match!` statement questions (7 messages, latest: Apr 24 2024 at 10:48)
- ✔ Unexpected indenting of coq terms (2 messages, latest: Apr 11 2024 at 06:57)
- Unexpected indenting of coq terms (11 messages, latest: Apr 10 2024 at 12:46)
- ✔ Program mode with tactics in terms (2 messages, latest: Apr 09 2024 at 18:03)
- Program mode with tactics in terms (3 messages, latest: Apr 09 2024 at 16:30)
- Preterm vs Constr.Unsafe (7 messages, latest: Mar 25 2024 at 12:16)
- ConstrMap (42 messages, latest: Mar 22 2024 at 16:27)
- Manipulation under a binder (5 messages, latest: Mar 22 2024 at 03:37)
- ✔ `occurn` (6 messages, latest: Mar 12 2024 at 17:57)
- Print type of term in ltac2, including implicts (11 messages, latest: Mar 11 2024 at 21:53)
- How to check if the context is empty in Ltac? (9 messages, latest: Feb 21 2024 at 14:56)
- Ltac2 Commands? (6 messages, latest: Feb 14 2024 at 21:19)
- module interaction API (11 messages, latest: Feb 08 2024 at 10:20)
- Working with evars and goals (6 messages, latest: Feb 04 2024 at 14:21)
- Differences between Ltac2 constr context and usual context (2 messages, latest: Jan 21 2024 at 02:07)
- Working with bound variables (2 messages, latest: Jan 20 2024 at 17:19)
- Performance Debugging Help? (5 messages, latest: Dec 24 2023 at 08:28)
- Hiding of local names in assert (17 messages, latest: Dec 08 2023 at 09:38)
- Coq `Search` through Ltac2 (12 messages, latest: Dec 06 2023 at 12:20)
- non_exhaustive (9 messages, latest: Dec 05 2023 at 17:13)
- open type extension with nothing (1 message, latest: Dec 05 2023 at 13:26)
- ✔ Unpacking lists of arguments (5 messages, latest: Dec 04 2023 at 16:14)
- Unpacking lists of arguments (3 messages, latest: Dec 04 2023 at 16:01)
- Use of variables in ltac1val quotation (8 messages, latest: Dec 04 2023 at 13:15)
- robust compatible Constr.Unsafe (3 messages, latest: Nov 14 2023 at 10:40)
- ✔ assert notation (7 messages, latest: Nov 10 2023 at 11:19)
- ✔ Arguments of Control.focus (2 messages, latest: Nov 09 2023 at 20:56)
- Arguments of Control.focus (2 messages, latest: Nov 09 2023 at 19:58)
- global mutable state (2 messages, latest: Oct 30 2023 at 23:04)
- ✔ Struggling to continue after an `assert (...) by ...` (6 messages, latest: Oct 12 2023 at 09:32)
- Early typing of Ltac2 Notations? (2 messages, latest: Oct 06 2023 at 08:47)
- Ltac2 tactic index (17 messages, latest: Oct 03 2023 at 08:43)
- ✔ Use of Ltac1.run, Ltac1.apply and Ltac1.of_ident (4 messages, latest: Sep 19 2023 at 07:33)
- Use of Ltac1.run, Ltac1.apply and Ltac1.of_ident (2 messages, latest: Sep 18 2023 at 15:07)
- ✔ CompCert exploit tactic in Ltac2 (4 messages, latest: Sep 08 2023 at 18:10)
- CompCert exploit tactic in Ltac2 (3 messages, latest: Sep 08 2023 at 10:22)
- Ltac2 Eval Std.unify (3 messages, latest: Sep 07 2023 at 21:44)
- Case analysis in pure Ltac2? (11 messages, latest: Jul 22 2023 at 20:18)
- ✔ `pose proof` in ltac2? (5 messages, latest: Jun 29 2023 at 12:22)
- Ltac2 debugger (19 messages, latest: May 19 2023 at 08:02)
- Convert Ltac1 integer to Ltac2 integer (2 messages, latest: May 14 2023 at 14:36)
- Pass value from ltac2 back to ltac1 (10 messages, latest: May 09 2023 at 11:38)
- Calling Ltac2 from OCaml (8 messages, latest: Apr 21 2023 at 16:26)
- Independence from stdlib (8 messages, latest: Apr 12 2023 at 16:08)
- Setting of mutable Ltac definitions from tactic (17 messages, latest: Mar 08 2023 at 09:30)
- 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: Oct 13 2024 at 01:02 UTC