Topics:
- Doing better than a Trusted Theory Base (38 messages, latest: Dec 09 2022 at 01:58)
- Translation to W types? (6 messages, latest: Dec 08 2022 at 21:49)
- Merging PRs (3 messages, latest: Dec 08 2022 at 09:31)
- ✔ `cored` and `extends_decls` (5 messages, latest: Dec 08 2022 at 09:29)
- Changing global universes in typing (7 messages, latest: Dec 07 2022 at 22:39)
- `cored` and `extends_decls` (14 messages, latest: Dec 07 2022 at 22:21)
- 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)
- Global environment extension modulo ordering (14 messages, latest: Nov 24 2022 at 11:36)
- 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)
- uGraph.consistent_ext_on_full_ext (13 messages, latest: Nov 23 2022 at 13:55)
- ✔ ConstraintSet.t -> LevelSet.t (2 messages, latest: Nov 23 2022 at 13:52)
- ✔ quoting `valid_constraints` for quoting typing judgments (2 messages, latest: Nov 23 2022 at 13:51)
- ✔ Checking universe graph? (2 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 (1 message, latest: Nov 23 2022 at 13:10)
- guard checker (4 messages, latest: Nov 23 2022 at 12:51)
- Checking universe graph? (3 messages, latest: Nov 23 2022 at 12:51)
- quoting `valid_constraints` for quoting typing judgments (38 messages, latest: Nov 23 2022 at 12:40)
- 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` (1 message, latest: Nov 07 2022 at 23:10)
- ✔ Build errors (1 message, latest: Nov 07 2022 at 23:10)
- ✔ Template.TypingWf.on_option (2 messages, latest: Nov 07 2022 at 23:08)
- ✔ Typing.v Prop vs bool (2 messages, latest: Nov 07 2022 at 23:08)
- Template.TypingWf.on_option (3 messages, latest: Nov 07 2022 at 20:21)
- Typing.v Prop vs bool (2 messages, latest: Nov 07 2022 at 14:17)
- ConstraintSet.t -> LevelSet.t (1 message, latest: Nov 04 2022 at 18:21)
- 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)
- Build errors (16 messages, latest: Oct 28 2022 at 17:57)
- `on_ind_body` (5 messages, latest: Oct 26 2022 at 17:10)
- 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 (2 messages, latest: Oct 24 2022 at 11:16)
- Implicits intros in tmLemma (12 messages, latest: Oct 24 2022 at 10:55)
- 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` (10 messages, latest: Oct 10 2022 at 13:41)
- Why is wf_local is not mutual recursion with `typing` (23 messages, latest: Oct 08 2022 at 13:01)
- 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: Dec 09 2022 at 08:02 UTC