Topics:
- 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 (10 messages, latest: Jul 12 2021 at 09:55)
- Some low-level questions about consistent (7 messages, latest: Jul 12 2021 at 08:51)
- Notation clash with Int63 (3 messages, latest: Jul 11 2021 at 15:02)
- opam install not working (59 messages, latest: Jun 25 2021 at 16:03)
- CI (16 messages, latest: Jun 09 2021 at 16:20)
- 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)
- stream events (1 message, latest: May 07 2020 at 09:05)
- imported from gitter room coq/metacoq (346 messages, latest: May 06 2020 at 01:59)
Last updated: Sep 26 2021 at 08:02 UTC