Topics:
- Reduce tactic arguments (3 messages, latest: Sep 24 2024 at 12:35)
- Extending predicate with multiple clauses (3 messages, latest: Sep 24 2024 at 11:09)
- ✔ std.forall vs manual loop (7 messages, latest: Sep 20 2024 at 09:12)
- std.forall vs manual loop (7 messages, latest: Sep 20 2024 at 09:01)
- ✔ elpi documentation (2 messages, latest: Sep 18 2024 at 13:47)
- elpi documentation (11 messages, latest: Sep 18 2024 at 12:46)
- Using Coq identifier in Elpi tactic (2 messages, latest: Sep 11 2024 at 19:40)
- Building elpi and coq_elpi in a dune workspace (70 messages, latest: Sep 05 2024 at 15:20)
- Literate programming (8 messages, latest: Sep 02 2024 at 15:49)
- Code review for homemade rewrite (9 messages, latest: Aug 26 2024 at 17:02)
- Compilation of coq-elpi on Coq master (10 messages, latest: Aug 14 2024 at 09:31)
- Multiple bangs in 1 rule (3 messages, latest: Jul 25 2024 at 16:10)
- opam semantics and rebuilds (9 messages, latest: Jul 15 2024 at 20:33)
- mathcomp/mathcomp:2.2.0-coq-dev FTBFS since today b/o elpi (2 messages, latest: Jun 24 2024 at 21:05)
- Elpi 1.14.3 for Coq 8.15 stopped to compile 2 nights back (6 messages, latest: May 24 2024 at 11:56)
- Search command (8 messages, latest: May 23 2024 at 13:41)
- synterp frustration (12 messages, latest: May 13 2024 at 14:56)
- Pattern on the LHS not equivalent to unification on the RHS? (5 messages, latest: Apr 17 2024 at 14:51)
- Import Coq module in elpi file (3 messages, latest: Apr 05 2024 at 13:42)
- Sharing code between multiple commands (4 messages, latest: Apr 04 2024 at 21:10)
- Matching on primitive projections (6 messages, latest: Mar 22 2024 at 23:15)
- ✔ Type synonyms? (1 message, latest: Mar 21 2024 at 22:43)
- Type synonyms? (3 messages, latest: Mar 21 2024 at 21:00)
- Release of coq-elpi (5 messages, latest: Mar 20 2024 at 21:53)
- Unable to graft clause (14 messages, latest: Mar 13 2024 at 18:48)
- Unknown Db in clients of elpi command in 8.19 (38 messages, latest: Mar 11 2024 at 14:00)
- elpi -> ltac1 -> vm_compute = normal cast (26 messages, latest: Mar 07 2024 at 14:19)
- ✔ Question on modes (4 messages, latest: Mar 04 2024 at 11:17)
- ✔ How to get the type of a term (2 messages, latest: Mar 04 2024 at 10:37)
- How to get the type of a term (2 messages, latest: Mar 04 2024 at 09:46)
- ✔ What does `clause` really do? (10 messages, latest: Feb 29 2024 at 12:46)
- Synterp/interp phase in NES (2 messages, latest: Feb 26 2024 at 13:10)
- coq.env.add-const error messages (13 messages, latest: Feb 22 2024 at 08:34)
- Custom attributes for derive extensions (3 messages, latest: Feb 21 2024 at 16:53)
- Dependencies between databases (5 messages, latest: Feb 20 2024 at 15:30)
- Derive extensions defining modules (37 messages, latest: Feb 16 2024 at 19:59)
- coq-elpi dev failing (5 messages, latest: Feb 16 2024 at 09:12)
- Assertion failed on calling coq.term->string in coq_elpi_HOA (3 messages, latest: Jan 29 2024 at 15:16)
- Analogous of `(DB => Clause)` on CHR (5 messages, latest: Jan 18 2024 at 10:26)
- Question on `decl` and `pi` (6 messages, latest: Jan 18 2024 at 10:12)
- coq.say but silent on make (3 messages, latest: Jan 17 2024 at 22:52)
- ✔ Analogous of `(DB => Clause)` on CHR (4 messages, latest: Jan 17 2024 at 15:58)
- Module enumeration (again) (3 messages, latest: Jan 17 2024 at 08:30)
- elpi Programs in Sections (4 messages, latest: Jan 16 2024 at 23:10)
- Different behavior between coq's unification and coqunify-eq (1 message, latest: Jan 10 2024 at 16:48)
- Undeclared macro exception (26 messages, latest: Jan 04 2024 at 21:34)
- OCaml 4.10 and later constraint (1 message, latest: Dec 29 2023 at 20:29)
- Error: Ill-typed evar instance (8 messages, latest: Dec 14 2023 at 11:47)
- ✔ Clause is not loaded (4 messages, latest: Dec 05 2023 at 16:57)
- Elaborate to Unification problem outside pattern fragment (6 messages, latest: Nov 30 2023 at 09:47)
- coq.typecheck introduces non-HOAS term (2 messages, latest: Nov 27 2023 at 16:38)
- Create free coq name (6 messages, latest: Nov 27 2023 at 16:32)
- ✔ Check if term uses undeclared constants (2 messages, latest: Nov 20 2023 at 14:02)
- Check if term uses undeclared constants (7 messages, latest: Nov 19 2023 at 09:01)
- coq.term->gref raises fatal errors (7 messages, latest: Nov 15 2023 at 13:33)
- Coq Platform pick (3 messages, latest: Nov 15 2023 at 10:51)
- Infinite loop when using coq.elaborate-skeleton (10 messages, latest: Nov 14 2023 at 10:22)
- Performance bottleneck in UState.demote_global_univs (2 messages, latest: Nov 12 2023 at 20:34)
- ✔ Assertion failed in coq_elpi_HOAS.ml (4 messages, latest: Nov 10 2023 at 14:15)
- Assertion failed in coq_elpi_HOAS.ml (2 messages, latest: Nov 10 2023 at 14:00)
- Elpi REPL (5 messages, latest: Nov 07 2023 at 14:32)
- Elpi Unification failure (20 messages, latest: Nov 07 2023 at 14:32)
- Contributing to Elpi, quoting (7 messages, latest: Oct 31 2023 at 15:10)
- VsCoq and elpi lang plugin (4 messages, latest: Oct 31 2023 at 14:37)
- `coercion` never called (15 messages, latest: Oct 30 2023 at 16:18)
- ✔ Coercion to Funclass (4 messages, latest: Oct 25 2023 at 06:52)
- Canonical instanciation via elpi (4 messages, latest: Oct 24 2023 at 14:37)
- ✔ Grafting in an implication (1 message, latest: Oct 24 2023 at 14:35)
- ✔ Typeclass instanciation via elpi (4 messages, latest: Oct 24 2023 at 14:33)
- Typeclass instanciation via elpi (9 messages, latest: Oct 24 2023 at 13:54)
- Grafting in an implication (5 messages, latest: Oct 19 2023 at 16:32)
- syntax scopes in raw arguments for commands (8 messages, latest: Oct 19 2023 at 14:20)
- Ill-typed evar instance (6 messages, latest: Oct 18 2023 at 11:37)
- coq-elpi primitive projections (29 messages, latest: Oct 17 2023 at 18:24)
- Non-determinism? (9 messages, latest: Oct 12 2023 at 13:06)
- Resolving Extra Dependencies (10 messages, latest: Oct 12 2023 at 11:43)
- ✔ Non-determinism? (5 messages, latest: Oct 10 2023 at 14:57)
- Unification variables as name in type (11 messages, latest: Oct 06 2023 at 17:47)
- ✔ Elaboration errors (12 messages, latest: Sep 28 2023 at 11:45)
- Catch elpi tactics failures with try (5 messages, latest: Sep 28 2023 at 11:38)
- ELPI Hacks (9 messages, latest: Sep 28 2023 at 09:31)
- ✔ intropatterns in tactic (1 message, latest: Sep 27 2023 at 15:15)
- intropatterns in tactic (4 messages, latest: Sep 27 2023 at 14:15)
- ✔ renaming when opening a sealed goal (3 messages, latest: Sep 25 2023 at 12:44)
- renaming when opening a sealed goal (6 messages, latest: Sep 25 2023 at 12:00)
- Coq-ELPI API (16 messages, latest: Aug 30 2023 at 13:00)
- Binding Elpi (11 messages, latest: Aug 30 2023 at 11:27)
- Elpi vs. TC/CS proof search (2 messages, latest: Aug 28 2023 at 12:06)
- ✔ Definitions shared between commands (2 messages, latest: Aug 09 2023 at 17:17)
- Definitions shared between commands (3 messages, latest: Aug 09 2023 at 16:49)
- Reasoning about λProlog programs (9 messages, latest: Aug 04 2023 at 21:21)
- Coq-Elpi tag for 8.18 (5 messages, latest: Aug 04 2023 at 12:23)
- refine failure when everything typechecks (2 messages, latest: Jul 06 2023 at 18:31)
- purge_algebraic_universes (3 messages, latest: Jun 30 2023 at 12:56)
- `derive` attribute parsing (6 messages, latest: Jun 26 2023 at 21:18)
- coq-elpi dev package CI error (6 messages, latest: Jun 16 2023 at 06:28)
- Pygments/minted theme for Coq-Elpi (6 messages, latest: Jun 13 2023 at 12:00)
- Inconsistent variable printing (5 messages, latest: Jun 01 2023 at 12:33)
- Design pattern: collecting info in the constraint store (2 messages, latest: May 16 2023 at 14:28)
- declare_constraint does not carry the context (5 messages, latest: May 16 2023 at 11:46)
- Macro tutorial (4 messages, latest: May 15 2023 at 15:22)
- Paper Recommendation by Amy Felty (1 message, latest: May 12 2023 at 19:51)
- Index syntax (2 messages, latest: May 11 2023 at 18:43)
- Execution order with spilling (3 messages, latest: May 05 2023 at 13:28)
- Dynlink error (4 messages, latest: Apr 13 2023 at 16:23)
- Backtracking & CHR (8 messages, latest: Apr 12 2023 at 09:01)
- Unusual error (7 messages, latest: Apr 05 2023 at 16:12)
- Hint databases (4 messages, latest: Apr 05 2023 at 12:26)
- Requiring Elpi makes `lib.` a syntax error (10 messages, latest: Mar 29 2023 at 20:49)
- Coq documentation (9 messages, latest: Mar 20 2023 at 10:26)
- Lambda clam (25 messages, latest: Mar 19 2023 at 19:46)
- Interaction between ocaml and coq-ELPI (1 message, latest: Mar 14 2023 at 10:43)
- Prolog extension for Monte Carlo Proof Search (4 messages, latest: Mar 09 2023 at 12:44)
- Flexible term outside pattern fragment (2 messages, latest: Mar 08 2023 at 20:44)
- Code behaving differently in commands and tactics (4 messages, latest: Mar 02 2023 at 10:24)
- Difference between var and uvar (4 messages, latest: Feb 27 2023 at 21:03)
- Adding a clause with a body to the context (4 messages, latest: Feb 27 2023 at 11:10)
- Association list of variables encoded in CHR + same_var (14 messages, latest: Feb 22 2023 at 13:52)
- Hide std.map type (3 messages, latest: Feb 07 2023 at 15:34)
- opam install coq-elpi (7 messages, latest: Jan 30 2023 at 22:21)
- app constructor (1 message, latest: Jan 27 2023 at 08:38)
- Generating proof terms containing Ltac (6 messages, latest: Jan 23 2023 at 09:33)
- Elpi Deriving (15 messages, latest: Jan 17 2023 at 17:18)
- ✔ Non closed Term (12 messages, latest: Dec 21 2022 at 15:38)
- ✔ Reducing integers (4 messages, latest: Dec 20 2022 at 20:44)
- Why did Elpi ended up looking like Elpi (5 messages, latest: Dec 11 2022 at 00:01)
- `.glob` entries from elpi (7 messages, latest: Dec 01 2022 at 11:05)
- Derive the name of the enclosing file level module (9 messages, latest: Nov 24 2022 at 14:57)
- Local version of coq.locate (2 messages, latest: Nov 19 2022 at 20:23)
- Preprocessing before itauto (7 messages, latest: Nov 15 2022 at 10:42)
- ✔ Using Query on a Db (4 messages, latest: Nov 11 2022 at 16:29)
- ✔ When does coq.elpi.accumulate take effect? (4 messages, latest: Nov 10 2022 at 15:48)
- coq.elaborate-skeleton generates fresh universes (12 messages, latest: Nov 10 2022 at 15:24)
- Typo in new Coq-Elpi tag (2 messages, latest: Nov 10 2022 at 13:58)
- ✔ Coq Platform CI failure (28 messages, latest: Nov 03 2022 at 18:18)
- Quotation for `constructor` (17 messages, latest: Oct 28 2022 at 08:51)
- Non-deterministic pruning (6 messages, latest: Oct 27 2022 at 08:57)
- How inspect terms under binders in Elpi (11 messages, latest: Oct 26 2022 at 13:18)
- ✔ Question on tutorial (4 messages, latest: Oct 26 2022 at 09:52)
- unknown inductive error on match (5 messages, latest: Oct 25 2022 at 09:34)
- use of copy with variables (17 messages, latest: Oct 24 2022 at 13:10)
- ELPI plugin for VSCodium (11 messages, latest: Oct 17 2022 at 15:03)
- Collecting constructor arguments (13 messages, latest: Oct 12 2022 at 12:59)
- LGPL license of examples and `apps` in coq-elpi (7 messages, latest: Oct 12 2022 at 08:27)
- Performance of wrapping `decide equality` (6 messages, latest: Oct 12 2022 at 00:43)
- Error "Not Yet Implemented: HOAS SFBmind" with Module API (31 messages, latest: Oct 11 2022 at 16:03)
- Possible bug related to implicit arguments (7 messages, latest: Oct 07 2022 at 21:00)
- Error `Not a variable after goal` (4 messages, latest: Oct 04 2022 at 14:19)
- fix constructor argument (3 messages, latest: Sep 26 2022 at 13:36)
- Recursive Elpi tactic, or predicate modifying the goal (15 messages, latest: Sep 23 2022 at 14:09)
- ✔ [beginner] Arguments of a tactic defined with `Elpi` (5 messages, latest: Sep 19 2022 at 19:09)
- Reifying terms with ltac / if-then-else / complex match (19 messages, latest: Sep 15 2022 at 16:29)
- ✔ Elpi tactic returning a term (7 messages, latest: Sep 14 2022 at 10:38)
- ✔ Outputting a list of variables (13 messages, latest: Sep 14 2022 at 10:38)
- ✔ Problem of unifying evars? (6 messages, latest: Sep 14 2022 at 10:38)
- Error "Unification problem outside the pattern fragment." (6 messages, latest: Sep 07 2022 at 14:11)
- Accumulate to a database during execution (3 messages, latest: Sep 01 2022 at 14:12)
- Running issues (5 messages, latest: Aug 18 2022 at 12:31)
- Issues with latest Elpi on Windows (11 messages, latest: Aug 13 2022 at 19:51)
- Proof obligations (4 messages, latest: Aug 12 2022 at 20:31)
- all_different constraint (5 messages, latest: Aug 03 2022 at 08:31)
- Calling external tools with Coq-Elpi (12 messages, latest: Jul 22 2022 at 20:47)
- Using `abstract` from Ltac1 in Elpi (10 messages, latest: Jul 22 2022 at 20:09)
- Recursive Predicate (4 messages, latest: Jul 20 2022 at 13:00)
- State Injectivity (19 messages, latest: Jul 20 2022 at 09:53)
- Question on error message "Evaluation of a non closed term" (8 messages, latest: Jul 20 2022 at 07:16)
- ✔ !tactic_mode (9 messages, latest: Jul 16 2022 at 20:36)
- ✔ Adding universe polymorphic inductive type (8 messages, latest: Jul 16 2022 at 20:36)
- `idtac` and then `clearbody`on a list (of lists) of terms (9 messages, latest: Jul 08 2022 at 08:37)
- Unifying a sort with Set (6 messages, latest: Jul 06 2022 at 17:08)
- Unification variable under binders (2 messages, latest: May 19 2022 at 20:02)
- coq-elpi on `coq.dev` again (23 messages, latest: May 15 2022 at 23:40)
- ✔ Spilling under a binder (14 messages, latest: May 11 2022 at 08:42)
- Removing a clause from an Elpi database (6 messages, latest: May 09 2022 at 13:50)
- ✔ coq-elpi broken on `coq.dev`? (5 messages, latest: May 05 2022 at 17:27)
- Universe polymorphism (9 messages, latest: May 05 2022 at 07:16)
- Elpi applications besides HB (8 messages, latest: May 04 2022 at 08:41)
- Making this stream web-public (2 messages, latest: Apr 19 2022 at 08:30)
- stream events (2 messages, latest: Apr 16 2022 at 16:54)
- First experience report (5 messages, latest: Apr 15 2022 at 17:38)
- [Beginner question] about binding with `pi`and `decl` (3 messages, latest: Apr 13 2022 at 13:41)
- Definition of copy (2 messages, latest: Apr 11 2022 at 18:11)
- Question on occurs (11 messages, latest: Apr 07 2022 at 14:36)
- What is the syntax of comments? (3 messages, latest: Apr 05 2022 at 06:39)
- New elpi variables when asserting a new goal (7 messages, latest: Apr 04 2022 at 11:59)
- Elpi version for Coq Platform (3 messages, latest: Mar 21 2022 at 10:57)
- `Elpi Debug` (5 messages, latest: Mar 16 2022 at 09:13)
- mlock Implicits (19 messages, latest: Feb 28 2022 at 14:59)
- Find a hypothesis in a sealed-goal (4 messages, latest: Feb 25 2022 at 19:35)
- RawData data model (5 messages, latest: Feb 23 2022 at 10:47)
- Elpi as a Type Classes resolution engine (28 messages, latest: Feb 22 2022 at 16:48)
- Elpi API (2 messages, latest: Feb 18 2022 at 13:03)
- Support for fixpoints (12 messages, latest: Feb 17 2022 at 17:34)
- ✔ citation (4 messages, latest: Feb 14 2022 at 08:49)
- coq-elpi fails to build on mathcom-dev:coq-dev docker image (4 messages, latest: Feb 10 2022 at 09:16)
- elpi and coqdep (80 messages, latest: Feb 03 2022 at 13:51)
- `Elpi Accumulate File` and Coq's `LoadPath` (35 messages, latest: Feb 03 2022 at 13:07)
- Hint Resolve (7 messages, latest: Feb 01 2022 at 21:51)
- ✔ Generating terms via ltac in an [Elpi Command] (16 messages, latest: Jan 26 2022 at 21:55)
- Functors (6 messages, latest: Jan 25 2022 at 21:21)
- Functors Implementation tradeoff (4 messages, latest: Jan 25 2022 at 18:08)
- Parens / command parsing (5 messages, latest: Jan 20 2022 at 21:20)
- Hint Opaque (6 messages, latest: Jan 20 2022 at 20:27)
- Revert on section variable "forgotten" by an elpi tactic (2 messages, latest: Dec 09 2021 at 16:18)
- Opaque bodies (5 messages, latest: Dec 03 2021 at 06:21)
- Local context update (2 messages, latest: Nov 18 2021 at 14:33)
- Using Conversion in Elpi's OCaml API (4 messages, latest: Nov 08 2021 at 09:51)
- Updated tutorials (7 messages, latest: Sep 28 2021 at 14:38)
- Create new goal (assert in Elpi) (6 messages, latest: Sep 01 2021 at 17:55)
- Pure tactic (7 messages, latest: Aug 20 2021 at 08:50)
- Tactic populating database at runtime does not work (12 messages, latest: Jul 22 2021 at 12:36)
- Abstract over "derive" (2 messages, latest: Jul 16 2021 at 05:41)
- Use case of induction over rose trees (2 messages, latest: Jul 13 2021 at 16:30)
- Print context (8 messages, latest: Jul 07 2021 at 09:48)
- Duplicate context entry (5 messages, latest: Jul 02 2021 at 12:45)
- Unification variable depending on term (31 messages, latest: Jul 02 2021 at 10:06)
- No notion of scope (10 messages, latest: Jun 29 2021 at 17:02)
- ease of debugging (5 messages, latest: Jun 03 2021 at 16:38)
- Elpi does not find database (6 messages, latest: Jun 02 2021 at 14:23)
- cut type error (3 messages, latest: Jun 01 2021 at 14:47)
- Inlining files containing `Elpi Accumulate File` (6 messages, latest: May 25 2021 at 07:33)
- Record Import (6 messages, latest: Apr 30 2021 at 06:29)
- Using Elpi with Emacs/PG (6 messages, latest: Apr 30 2021 at 06:09)
- coq-elpi.dev fails to build against coq.dev (16 messages, latest: Apr 25 2021 at 07:55)
- Predicate to associate Elpi `int` and Coq terms of `N` (7 messages, latest: Apr 22 2021 at 08:31)
- Abstract function application (5 messages, latest: Apr 15 2021 at 10:32)
- Generating large Coq term of type `list N` in Elpi (17 messages, latest: Apr 10 2021 at 16:38)
- Forcing garbage collection (2 messages, latest: Apr 10 2021 at 11:30)
- Set merge does not remove duplicates (3 messages, latest: Mar 04 2021 at 16:35)
- Synthesizing an Elpi clause from a Coq term with holes (6 messages, latest: Feb 28 2021 at 17:30)
- matching with function application (5 messages, latest: Feb 22 2021 at 11:37)
- new proof context variables or definitions (17 messages, latest: Feb 19 2021 at 07:17)
- Rewrite in Coq-Elpi (3 messages, latest: Feb 18 2021 at 20:04)
- Goal manipulation (3 messages, latest: Feb 18 2021 at 05:39)
- Map with Coq terms as keys (3 messages, latest: Feb 11 2021 at 16:47)
- Renaming a subterm (8 messages, latest: Feb 09 2021 at 11:16)
- Creating a Coq function in Coq-Elpi (7 messages, latest: Feb 08 2021 at 14:42)
- Custom reduction (14 messages, latest: Jan 25 2021 at 19:16)
- Typing in coq-elpi (4 messages, latest: Jan 25 2021 at 17:03)
- Elpi goal rewriting (4 messages, latest: Dec 01 2020 at 14:39)
- coq-elpi fails to build on coqorg/coq:dev docker image (12 messages, latest: Nov 30 2020 at 15:51)
- Support for mutually inductive types (8 messages, latest: Nov 25 2020 at 14:10)
- inductive predicate to boolean function (9 messages, latest: Nov 14 2020 at 13:15)
- Elpi on Windows (21 messages, latest: Sep 16 2020 at 13:50)
- Tactician (21 messages, latest: Sep 12 2020 at 17:25)
- Examples (2 messages, latest: Aug 30 2020 at 06:28)
Last updated: Oct 13 2024 at 01:02 UTC