Topics:
- default branch (1 message, latest: Sep 30 2023 at 04:23)
- Theorems about inductive type descriptions (11 messages, latest: Sep 13 2023 at 16:19)
- MetaCoq for AST generation (27 messages, latest: Aug 17 2023 at 07:11)
- Constructing Records and Classes (11 messages, latest: Jul 13 2023 at 17:03)
- Call for help: Rosetta stone for Metaprogramming in Coq (5 messages, latest: Jun 28 2023 at 18:28)
- Magmide (8 messages, latest: Jun 24 2023 at 14:23)
- Merge Policy (1 message, latest: Jun 19 2023 at 14:12)
- PR Review? (45 messages, latest: Jun 03 2023 at 23:50)
- erasurefunction taking lots of memory? (5 messages, latest: May 27 2023 at 16:08)
- Performance Info (12 messages, latest: May 22 2023 at 11:07)
- Soundness vs Strong Normalization (14 messages, latest: May 16 2023 at 09:00)
- SafeChecker invocation? (14 messages, latest: Apr 26 2023 at 09:01)
- Universes of term? (5 messages, latest: Apr 26 2023 at 07:12)
- Monad utils / new ExtLib dependency (3 messages, latest: Apr 25 2023 at 07:32)
- 8.17 version / Coq Platform 2022.03 beta (24 messages, latest: Apr 24 2023 at 19:20)
- SafeChecker on open terms? (16 messages, latest: Apr 19 2023 at 20:36)
- Non-squashed typing judgments (58 messages, latest: Apr 18 2023 at 15:02)
- `type_mkApps` (2 messages, latest: Apr 17 2023 at 07:26)
- ✔ generalizing from typing in the empty context (4 messages, latest: Apr 14 2023 at 22:36)
- generalizing from typing in the empty context (6 messages, latest: Apr 14 2023 at 21:58)
- sync 8.16 and master branches (2 messages, latest: Apr 13 2023 at 10:16)
- PCUIC Quotation (1 message, latest: Apr 13 2023 at 08:05)
- understanding inductive types (40 messages, latest: Apr 11 2023 at 11:27)
- ✔ maste (1 message, latest: Apr 11 2023 at 06:12)
- maste (3 messages, latest: Apr 05 2023 at 06:22)
- Gallina quotation (2 messages, latest: Apr 05 2023 at 01:30)
- Fixing dynlink errors? (3 messages, latest: Apr 03 2023 at 10:12)
- Nix CI broken? (22 messages, latest: Apr 03 2023 at 06:40)
- Options in `tm_util` (8 messages, latest: Mar 30 2023 at 08:15)
- tmTry (5 messages, latest: Mar 26 2023 at 20:47)
- CI failure (52 messages, latest: Mar 23 2023 at 13:28)
- ✔ Error when stepping the code from erasure_live_test.v (16 messages, latest: Mar 06 2023 at 10:44)
- Frustrating universe errors? (6 messages, latest: Feb 28 2023 at 05:14)
- tmExistingInstance (3 messages, latest: Feb 28 2023 at 04:40)
- segfaults? (3 messages, latest: Feb 28 2023 at 04:39)
- compilation errors not in the wiki (3 messages, latest: Feb 24 2023 at 15:52)
- TemplateMonad and SProp? (1 message, latest: Feb 21 2023 at 23:25)
- tmQuoteModule deficiencies (2 messages, latest: Feb 21 2023 at 20:44)
- mkLambda / closing a locally nameless term (3 messages, latest: Feb 14 2023 at 21:28)
- universe constraints in template monad programs (1 message, latest: Feb 14 2023 at 02:55)
- global_reference -> term in the template monad (1 message, latest: Feb 14 2023 at 02:35)
- Template and PCUIC (4 messages, latest: Feb 13 2023 at 13:59)
- Gallina quotation functions (9 messages, latest: Feb 12 2023 at 03:25)
- Build errors (coq#17022) (2 messages, latest: Feb 08 2023 at 15:50)
- Build errors (coq#17021) (7 messages, latest: Jan 17 2023 at 14:58)
- running TemplateMonad inside a tactic (6 messages, latest: Jan 14 2023 at 12:43)
- plugins in MetaCoq vs. ML (4 messages, latest: Dec 27 2022 at 11:11)
- Build errors (12 messages, latest: Dec 15 2022 at 10:52)
- Global environment extension modulo ordering (15 messages, latest: Dec 14 2022 at 16:29)
- Why `extends_decls` in `PCUICElimination.Informative` (2 messages, latest: Dec 13 2022 at 11:56)
- Doing better than a Trusted Theory Base (55 messages, latest: Dec 09 2022 at 22:58)
- uGraph.consistent_ext_on_full_ext (14 messages, latest: Dec 09 2022 at 12:38)
- Translation to W types? (8 messages, latest: Dec 09 2022 at 11:01)
- Merging PRs (3 messages, latest: Dec 08 2022 at 09:31)
- ✔ `cored` and `extends_decls` (19 messages, latest: Dec 08 2022 at 09:29)
- Changing global universes in typing (7 messages, latest: Dec 07 2022 at 22:39)
- Stack overflow during a tactic (4 messages, latest: Dec 07 2022 at 16:21)
- Template Monad universes (1 message, latest: Nov 28 2022 at 19:26)
- extends (2 messages, latest: Nov 27 2022 at 20:16)
- template-coq/gen-src/cRelationClasses.mli.orig (1 message, latest: Nov 25 2022 at 00:44)
- Axioms vs (typeclass) hypotheses (9 messages, latest: Nov 25 2022 at 00:44)
- Set Suggest Proof Using (17 messages, latest: Nov 24 2022 at 20:33)
- Proving typing of `<% ... %>` (19 messages, latest: Nov 24 2022 at 18:58)
- Prop (12 messages, latest: Nov 24 2022 at 11:33)
- inspect on recursive calls (7 messages, latest: Nov 24 2022 at 11:31)
- Lack of decidable equality (32 messages, latest: Nov 24 2022 at 11:29)
- adding False to Σ (1 message, latest: Nov 24 2022 at 00:07)
- ✔ ConstraintSet.t -> LevelSet.t (3 messages, latest: Nov 23 2022 at 13:52)
- ✔ quoting `valid_constraints` for quoting typing judgments (40 messages, latest: Nov 23 2022 at 13:51)
- ✔ Checking universe graph? (5 messages, latest: Nov 23 2022 at 13:50)
- Non-squashed typing judgments? (3 messages, latest: Nov 23 2022 at 13:40)
- tmUnquote (4 messages, latest: Nov 23 2022 at 13:38)
- ✔ guard checker (5 messages, latest: Nov 23 2022 at 13:10)
- Debugging anomalies (2 messages, latest: Nov 23 2022 at 12:38)
- Free variables? (8 messages, latest: Nov 23 2022 at 12:34)
- Working with PCUICAst (8 messages, latest: Nov 23 2022 at 12:22)
- `tmFix`point combinator (39 messages, latest: Nov 22 2022 at 00:10)
- Fueling the checker (20 messages, latest: Nov 11 2022 at 20:07)
- ✔ `on_ind_body` (6 messages, latest: Nov 07 2022 at 23:10)
- ✔ Build errors (17 messages, latest: Nov 07 2022 at 23:10)
- ✔ Template.TypingWf.on_option (5 messages, latest: Nov 07 2022 at 23:08)
- ✔ Typing.v Prop vs bool (4 messages, latest: Nov 07 2022 at 23:08)
- squashing in infer_template_program? (2 messages, latest: Nov 04 2022 at 06:30)
- Determining when a constant is global? (9 messages, latest: Oct 31 2022 at 17:29)
- mutual_inductive_entry (7 messages, latest: Oct 26 2022 at 13:42)
- Async fails to load MetaCoq (6 messages, latest: Oct 25 2022 at 17:42)
- ✔ Implicits intros in tmLemma (14 messages, latest: Oct 24 2022 at 11:16)
- properties of MetaCoq/PCUIC (32 messages, latest: Oct 22 2022 at 21:00)
- Tactics in MetaCoq (26 messages, latest: Oct 13 2022 at 08:55)
- ✔ Why is wf_local is not mutual recursion with `typing` (33 messages, latest: Oct 10 2022 at 13:41)
- Use of tmLemma (6 messages, latest: Oct 05 2022 at 21:12)
- MetaCoq 1.0 problems for 8.16 (49 messages, latest: Sep 22 2022 at 13:03)
- Reification of operations on Z (12 messages, latest: Aug 31 2022 at 15:41)
- CI (31 messages, latest: Aug 05 2022 at 10:38)
- Access the defined constant of tmMkInductive (8 messages, latest: Jul 06 2022 at 09:37)
- Typeclasses (4 messages, latest: Jun 28 2022 at 12:35)
- StackExchange on guard condition stuff (2 messages, latest: May 25 2022 at 12:15)
- Universes for new inductive (22 messages, latest: May 06 2022 at 17:30)
- stream events (2 messages, latest: May 04 2022 at 07:51)
- opam install metacoq-template does not work on MacOs (58 messages, latest: Apr 26 2022 at 13:22)
- REPL for MetaCoq? (61 messages, latest: Feb 15 2022 at 13:10)
- ✔ TemplateMonad: get constructors of inductive type (21 messages, latest: Jan 07 2022 at 10:00)
- Significance of template-coq record fields (23 messages, latest: Jan 07 2022 at 08:03)
- Way to call unquote from a coq function (11 messages, latest: Jan 07 2022 at 05:43)
- Descriptions of fields of record types in template-coq (4 messages, latest: Jan 03 2022 at 07:23)
- ✔ Definition of kername (7 messages, latest: Dec 30 2021 at 17:00)
- ✔ Error on trying add_constructor example (9 messages, latest: Dec 30 2021 at 10:36)
- The META file (3 messages, latest: Nov 30 2021 at 14:05)
- Infer implicit types during unquoting (24 messages, latest: Nov 12 2021 at 10:23)
- build failure on case insensitive filesystem (1 message, latest: Nov 08 2021 at 16:57)
- Certified OCaml extraction (8 messages, latest: Oct 13 2021 at 18:37)
- migrate metacoq to coq-hott (3 messages, latest: Oct 06 2021 at 20:50)
- How to speed up Metacoq compile time (35 messages, latest: Sep 02 2021 at 14:16)
- Strange Error when Compile PCUICWcbvEval.v (4 messages, latest: Aug 28 2021 at 07:41)
- Why the erasure target language is untyped? (6 messages, latest: Aug 23 2021 at 09:22)
- ✔ Notation clash with Int63 (13 messages, latest: Jul 12 2021 at 09:55)
- Some low-level questions about consistent (7 messages, latest: Jul 12 2021 at 08:51)
- opam install not working (59 messages, latest: Jun 25 2021 at 16:03)
- No rule to make target tm_util.cmx (16 messages, latest: Jun 06 2021 at 16:23)
- question about impredicative set (10 messages, latest: May 04 2021 at 06:52)
- Recursive Quote Tactic (3 messages, latest: Mar 04 2021 at 10:50)
- error from opam (24 messages, latest: Feb 16 2021 at 19:10)
- Make MetaCoq Run use a different reduction strategy (9 messages, latest: Dec 16 2020 at 19:34)
- Adding new types to the quoting mechanism (4 messages, latest: Dec 10 2020 at 13:21)
- Efficient substitutions For Reals (3 messages, latest: Dec 08 2020 at 18:19)
- Primitive types in MetaCoq (16 messages, latest: Dec 08 2020 at 13:04)
- Which meta-language to choose? (11 messages, latest: Dec 03 2020 at 16:10)
- Adding a un/quoted term (or its type) in the environment (11 messages, latest: Nov 30 2020 at 15:44)
- Failure in Coq's CI (7 messages, latest: Nov 19 2020 at 13:22)
- wf_universes and reduction (2 messages, latest: Nov 18 2020 at 11:59)
- MetaCoq depends on time command? (25 messages, latest: Oct 05 2020 at 13:28)
- MetaCoq CI / Coq Community CI (19 messages, latest: Oct 01 2020 at 17:25)
- Proving a reified proposition with Program (10 messages, latest: Sep 30 2020 at 08:01)
- errors in coq CI log (2 messages, latest: Sep 24 2020 at 14:34)
- Moving erased eval to Type (5 messages, latest: Sep 23 2020 at 13:00)
- de Bruijn indices while declaring inductive (5 messages, latest: Sep 22 2020 at 13:03)
- News (2 messages, latest: Sep 15 2020 at 19:46)
- red_proj, eval_proj and multi-constructor inductives (6 messages, latest: Sep 15 2020 at 19:23)
- Discarding tEvar (5 messages, latest: Sep 08 2020 at 13:55)
- OPAM version ordering fixes (11 messages, latest: Sep 07 2020 at 09:43)
- Quoting the current global environment (4 messages, latest: Sep 04 2020 at 12:25)
- Are typing derivations property ? (13 messages, latest: Aug 28 2020 at 09:15)
- Difference between existential variables and metavariables (4 messages, latest: Jul 31 2020 at 13:02)
- Trying out metacoq (41 messages, latest: Jul 28 2020 at 16:39)
- Erasure evaluation relation is nondeterministic (41 messages, latest: Jul 20 2020 at 09:30)
- New local assumption / weakening (8 messages, latest: Jul 06 2020 at 07:36)
- Parametericity translation (4 messages, latest: Jul 05 2020 at 14:31)
- Flag for typing judgments (4 messages, latest: Jul 03 2020 at 15:28)
- Mismatch about printed name of a constructor (4 messages, latest: Jun 30 2020 at 09:33)
- Compatibility with Equations 1.2.2 (4 messages, latest: Jun 26 2020 at 08:49)
- Dis/proving a meta-theoretical question (33 messages, latest: Jun 19 2020 at 15:07)
- Unquote and quote does work using Prop (14 messages, latest: Jun 12 2020 at 14:51)
- Shape of case branches (9 messages, latest: Jun 11 2020 at 09:07)
- tmUnquoteTyped (5 messages, latest: Jun 10 2020 at 08:43)
- hnf/reduce_term (22 messages, latest: Jun 04 2020 at 09:56)
- imported from gitter room coq/metacoq (346 messages, latest: May 06 2020 at 01:59)
Last updated: Sep 30 2023 at 05:01 UTC