Topics:
- No space left on device (11 messages, latest: Mar 23 2023 at 14:05)
- docker dev/master change? (7 messages, latest: Mar 23 2023 at 13:27)
- coq-bench for opam (740 messages, latest: Mar 22 2023 at 18:31)
- Finding all locations where a definition is unfolded (12 messages, latest: Mar 22 2023 at 17:08)
- coq call (472 messages, latest: Mar 22 2023 at 12:00)
- ✔ difference between 8.4 and 8.5 docker images? (9 messages, latest: Mar 20 2023 at 21:14)
- -fake-source (27 messages, latest: Mar 19 2023 at 23:50)
- itauto broken (27 messages, latest: Mar 17 2023 at 16:11)
- Hints.FullHint.pattern, replacement? (75 messages, latest: Mar 17 2023 at 16:04)
- cprofile (2 messages, latest: Mar 17 2023 at 13:24)
- Docker ToS change (11 messages, latest: Mar 17 2023 at 12:44)
- ✔ needs:rebase checker not working? (5 messages, latest: Mar 16 2023 at 14:37)
- macos CI issues? (1 message, latest: Mar 15 2023 at 15:45)
- Coq Release 8.17 (207 messages, latest: Mar 15 2023 at 09:10)
- Printing terms with longest qualid. (2 messages, latest: Mar 14 2023 at 22:23)
- PR 17118 (1 message, latest: Mar 14 2023 at 10:28)
- CoqIDE in 8.17 / master (9 messages, latest: Mar 10 2023 at 18:34)
- Issues about extraction (25 messages, latest: Mar 08 2023 at 19:58)
- make validate axioms (15 messages, latest: Mar 08 2023 at 17:15)
- Minimize bug without location (22 messages, latest: Mar 04 2023 at 22:01)
- dependent elimination and primitive records without eta (23 messages, latest: Mar 04 2023 at 17:44)
- dpdgraph (12 messages, latest: Mar 03 2023 at 15:12)
- new_type_evar returning a non-evar (8 messages, latest: Mar 03 2023 at 09:53)
- stdlib reviews (7 messages, latest: Mar 03 2023 at 08:00)
- Hint Constants Opaque breaks trivial unification problems? (11 messages, latest: Mar 02 2023 at 10:42)
- coq_tex codeowner (2 messages, latest: Mar 01 2023 at 09:10)
- GitHub tarball regeneration (67 messages, latest: Mar 01 2023 at 06:41)
- ✔ coq 8.17 rc1 and opam (3 messages, latest: Feb 28 2023 at 16:08)
- Plugins and grammars (11 messages, latest: Feb 28 2023 at 15:45)
- non-transitive module subtyping (2 messages, latest: Feb 28 2023 at 00:10)
- Profiling on Coq Plugin (6 messages, latest: Feb 27 2023 at 17:03)
- Extraction of sort-polymorphic types in Prop (1 message, latest: Feb 27 2023 at 11:29)
- Introduce Base.Hash as extra OCaml dependencies for Plugin (1 message, latest: Feb 24 2023 at 05:11)
- Local CI workflow (20 messages, latest: Feb 22 2023 at 21:26)
- ✔ getting the list of constants in a module (11 messages, latest: Feb 21 2023 at 21:48)
- Getting the path of the current file (41 messages, latest: Feb 20 2023 at 22:56)
- coq-lsp CI job failing (2 messages, latest: Feb 17 2023 at 15:06)
- Global state in a plugin (7 messages, latest: Feb 14 2023 at 14:08)
- CI failure in coq-elpi (9 messages, latest: Feb 10 2023 at 09:18)
- Merge queue (1 message, latest: Feb 09 2023 at 14:48)
- dockerfile update workers (2 messages, latest: Feb 09 2023 at 13:34)
- Plans for hints in proofs (27 messages, latest: Feb 09 2023 at 00:50)
- CI runners (1 message, latest: Feb 08 2023 at 15:57)
- Strange lexing error (10 messages, latest: Feb 08 2023 at 15:33)
- CI dependencies (6 messages, latest: Feb 08 2023 at 15:31)
- ✔ Writing a term of type Pp.t to a file (4 messages, latest: Feb 06 2023 at 18:09)
- Anomaly with unipoly, indexed inductives and number notation (1 message, latest: Feb 06 2023 at 17:15)
- Repeated deprecation warnings (5 messages, latest: Feb 05 2023 at 12:20)
- Coq Working Group February 2023 (97 messages, latest: Jan 31 2023 at 17:25)
- Upcoming GitLab CI storage limits (41 messages, latest: Jan 31 2023 at 15:19)
- Github discussion (7 messages, latest: Jan 26 2023 at 21:39)
- `kind: infrastructure` -> `part: infrastructure` (11 messages, latest: Jan 25 2023 at 20:54)
- could not find META.coq-core (9 messages, latest: Jan 25 2023 at 18:57)
- Universe Polymorphism incompatibilities (1 message, latest: Jan 25 2023 at 17:25)
- CUDW 2023? (23 messages, latest: Jan 25 2023 at 15:12)
- findlib and CI artifacts (1 message, latest: Jan 24 2023 at 16:50)
- ✔ `.coqrc` leaking into coq stdlib due to dune build? (13 messages, latest: Jan 23 2023 at 23:29)
- OCaml 5.0 patch (208 messages, latest: Jan 23 2023 at 06:41)
- Frequent POPL questions (10 messages, latest: Jan 22 2023 at 10:31)
- HB failures in CI (9 messages, latest: Jan 20 2023 at 20:13)
- doc:stdlib failures (3 messages, latest: Jan 20 2023 at 13:10)
- Notion of glueing in gramlib (12 messages, latest: Jan 20 2023 at 08:16)
- bedrock failing in CI (3 messages, latest: Jan 18 2023 at 11:19)
- Command to print current lemma statement (18 messages, latest: Jan 16 2023 at 17:43)
- Dune caching & Coq non-reproducible builds (23 messages, latest: Jan 15 2023 at 21:07)
- Github code scanning (48 messages, latest: Jan 11 2023 at 18:57)
- Motivations for extensible parsing (20 messages, latest: Jan 10 2023 at 22:21)
- Undoing Syntax Extensions (1 message, latest: Jan 09 2023 at 15:42)
- ✔ coqbot merge and squash (3 messages, latest: Jan 09 2023 at 15:22)
- Mac CI in fork branch (6 messages, latest: Jan 09 2023 at 12:15)
- Substitutivity of refine (4 messages, latest: Jan 08 2023 at 17:07)
- resubmission of Docker Hub Open-Source program application (7 messages, latest: Jan 07 2023 at 17:56)
- Coq-Ci needs full CI (28 messages, latest: Jan 05 2023 at 09:38)
- Legacy attributes (4 messages, latest: Jan 05 2023 at 09:27)
- switching HoTT to use Dune (17 messages, latest: Jan 03 2023 at 02:36)
- Permission denied during test-suite (1 message, latest: Dec 29 2022 at 17:43)
- upstream changes for num (3 messages, latest: Dec 20 2022 at 14:32)
- fiat-crypto CI timing (2 messages, latest: Dec 16 2022 at 17:57)
- OCaml 5.0 and Coq's CI (1 message, latest: Dec 16 2022 at 16:00)
- Pyml with dune for plugin (68 messages, latest: Dec 16 2022 at 15:36)
- Warnings in compat theories (11 messages, latest: Dec 15 2022 at 12:24)
- coq calls (102 messages, latest: Dec 14 2022 at 15:48)
- looking for assignee (1 message, latest: Dec 14 2022 at 09:08)
- Making a new attribute (20 messages, latest: Dec 13 2022 at 20:54)
- Async failure (20 messages, latest: Dec 11 2022 at 18:03)
- Deprecation deletion overwriting (15 messages, latest: Dec 10 2022 at 18:35)
- CI pipeline minutes running out (362 messages, latest: Dec 09 2022 at 16:27)
- reduced impredicative set? (16 messages, latest: Dec 09 2022 at 13:42)
- about warnings (3 messages, latest: Dec 09 2022 at 09:16)
- Job webhook disabled (5 messages, latest: Dec 08 2022 at 13:22)
- GitHub App permission review (4 messages, latest: Dec 07 2022 at 14:26)
- Grammar not current (8 messages, latest: Dec 07 2022 at 10:14)
- iris failing (29 messages, latest: Dec 05 2022 at 17:26)
- ✔ Logic.refiner (6 messages, latest: Dec 05 2022 at 13:10)
- ✔ Notation declaration datatype (8 messages, latest: Dec 05 2022 at 12:54)
- cmt and cmti files in plugins (1 message, latest: Dec 04 2022 at 11:03)
- Tips for Starting Contributing? (4 messages, latest: Dec 01 2022 at 08:56)
- Parts of website down? (27 messages, latest: Nov 29 2022 at 20:05)
- packaging 8.16 (4 messages, latest: Nov 28 2022 at 14:02)
- deprecated-instance-without-locality errors (30 messages, latest: Nov 27 2022 at 18:23)
- Runner running out of disk space? (2 messages, latest: Nov 27 2022 at 09:34)
- 8.16.1 released (14 messages, latest: Nov 25 2022 at 16:49)
- why not use overlays everywhere (compcert / vst waiting f... (49 messages, latest: Nov 25 2022 at 14:12)
- New Discourse topics (45 messages, latest: Nov 25 2022 at 12:19)
- compcert / vst waiting for overlay (1 message, latest: Nov 25 2022 at 09:04)
- Program mode and typeclasses (3 messages, latest: Nov 24 2022 at 21:10)
- Does `Register` persist outside of a section? (2 messages, latest: Nov 24 2022 at 18:59)
- Deprecated lemmas and upvoting issues (35 messages, latest: Nov 24 2022 at 16:59)
- Adding a new control vernacular using a plugin (9 messages, latest: Nov 24 2022 at 15:35)
- Deactivating `par:` process spawning (67 messages, latest: Nov 24 2022 at 15:14)
- full CI on innocuous PRs (6 messages, latest: Nov 24 2022 at 09:26)
- Missed inlining optimization (14 messages, latest: Nov 24 2022 at 08:54)
- Require Import in byte (11 messages, latest: Nov 23 2022 at 15:48)
- 32 bit broken (16 messages, latest: Nov 23 2022 at 11:58)
- canonical structures variants (1 message, latest: Nov 22 2022 at 02:08)
- Platform file hosting (12 messages, latest: Nov 21 2022 at 10:41)
- Coq org unused repos (9 messages, latest: Nov 21 2022 at 09:44)
- anomaly guessing game (3 messages, latest: Nov 19 2022 at 19:16)
- findlib needs the package to not be installed (7 messages, latest: Nov 15 2022 at 09:58)
- usr/doc/coq-core/README.md (1 message, latest: Nov 11 2022 at 15:07)
- 8.16.0 released (83 messages, latest: Nov 11 2022 at 12:18)
- Typeclass resolution algorithm? (15 messages, latest: Nov 06 2022 at 15:36)
- SerApi: how to make an opam based dev build? (9 messages, latest: Nov 04 2022 at 19:59)
- Moving the wiki off github? (2 messages, latest: Nov 02 2022 at 17:13)
- typeclasses eauto vs simple eapply (6 messages, latest: Nov 01 2022 at 00:55)
- determining if a functor is open (4 messages, latest: Oct 31 2022 at 17:32)
- Coq Platform Windows CI failing cause of cygwin changes (3 messages, latest: Oct 31 2022 at 16:01)
- Removed file warning (16 messages, latest: Oct 30 2022 at 12:17)
- ✔ dune build woes (13 messages, latest: Oct 28 2022 at 18:00)
- "Always suggest updating pull request branches" setting (7 messages, latest: Oct 28 2022 at 17:22)
- CI these days (6 messages, latest: Oct 28 2022 at 16:39)
- Coq Winter Working Group 2022/(2023?) (2 messages, latest: Oct 28 2022 at 15:02)
- Garbage collection time (27 messages, latest: Oct 26 2022 at 20:36)
- fiat crypto broken (32 messages, latest: Oct 26 2022 at 12:25)
- vst failing (38 messages, latest: Oct 24 2022 at 15:01)
- pipeline list (2 messages, latest: Oct 24 2022 at 09:21)
- Guard Checker (11 messages, latest: Oct 21 2022 at 21:52)
- 8.16 regression in ssreflect apply (173 messages, latest: Oct 21 2022 at 09:49)
- Runner failures on docker-machine runner (29 messages, latest: Oct 20 2022 at 23:17)
- Proofview monad snapshot (6 messages, latest: Oct 20 2022 at 16:09)
- Setup Development Environment for Coq Plugin (12 messages, latest: Oct 20 2022 at 12:42)
- evarsolve aliasing (7 messages, latest: Oct 20 2022 at 08:13)
- Bugs with lonely coq-core (35 messages, latest: Oct 19 2022 at 21:48)
- Dune strikes back (56 messages, latest: Oct 19 2022 at 21:26)
- native compilation and universe polymorphism (9 messages, latest: Oct 19 2022 at 13:39)
- Working out the type of bindings introduced by a case (4 messages, latest: Oct 19 2022 at 12:46)
- Runner failures on ci-coq-02-runner-* (6 messages, latest: Oct 19 2022 at 11:18)
- Confusing comment in the kernel (3 messages, latest: Oct 18 2022 at 16:34)
- bench (55 messages, latest: Oct 18 2022 at 07:18)
- windows failing (9 messages, latest: Oct 17 2022 at 15:46)
- Plugin depending on an internal library (78 messages, latest: Oct 17 2022 at 10:58)
- Runner failures (80 messages, latest: Oct 17 2022 at 07:19)
- ✔ Struggling with `make test-suite` (7 messages, latest: Oct 17 2022 at 04:36)
- Extraction and counting (3 messages, latest: Oct 16 2022 at 08:01)
- Actions taken on CI because of minutes running out (10 messages, latest: Oct 14 2022 at 22:41)
- Local run of the smtcoq CI (13 messages, latest: Oct 14 2022 at 16:24)
- opam packaging conf-? for ulimit (9 messages, latest: Oct 14 2022 at 14:58)
- pipeline timeout (10 messages, latest: Oct 14 2022 at 07:31)
- Debugging cyclicly defined evars (4 messages, latest: Oct 13 2022 at 16:27)
- Fixpoint values in the VM (43 messages, latest: Oct 13 2022 at 16:10)
- ✔ Use Micromega_plugin in another plugin, in Coq-8.16 (5 messages, latest: Oct 12 2022 at 08:22)
- ✔ .mlg files in vscode (18 messages, latest: Oct 11 2022 at 09:03)
- Unbound module Evd (6 messages, latest: Oct 10 2022 at 18:12)
- fiat-crypto looping (3 messages, latest: Oct 08 2022 at 11:05)
- Reopen closed PR on GitHub (10 messages, latest: Oct 07 2022 at 14:04)
- coq.gitlab.io issues and MR (10 messages, latest: Oct 06 2022 at 07:48)
- Nix job ran out of free space (9 messages, latest: Oct 05 2022 at 21:22)
- GitHub CI issues (4 messages, latest: Oct 05 2022 at 16:41)
- coqbot FULL_CI support (2 messages, latest: Oct 05 2022 at 16:23)
- roadmap (20 messages, latest: Oct 05 2022 at 12:32)
- `let` binders and kernel conversion (9 messages, latest: Oct 05 2022 at 11:24)
- failing coqide-server dev opam package (5 messages, latest: Oct 03 2022 at 09:11)
- in-repo coqide.dev vs opam archive (22 messages, latest: Oct 01 2022 at 22:56)
- Using "malfunction" for native code (130 messages, latest: Sep 30 2022 at 16:27)
- Renaming the shims (1 message, latest: Sep 28 2022 at 22:30)
- Error: Anomaly "Stm.join: tip not cached" (4 messages, latest: Sep 28 2022 at 21:36)
- Interim VsCoq maintenance (48 messages, latest: Sep 28 2022 at 19:50)
- coq.dev opam package not producing coqidetop.opt? (102 messages, latest: Sep 27 2022 at 16:02)
- Fall WG (5 messages, latest: Sep 26 2022 at 17:52)
- invariants of the tactic engine (6 messages, latest: Sep 26 2022 at 16:12)
- ✔ EConstr.Vars.subst_var (5 messages, latest: Sep 26 2022 at 15:35)
- ✔ EConstr.fold (3 messages, latest: Sep 26 2022 at 15:12)
- match elaboration and reduction (1 message, latest: Sep 24 2022 at 10:54)
- Too many pipelines (49 messages, latest: Sep 23 2022 at 11:11)
- Error on hint absence (2 messages, latest: Sep 20 2022 at 15:21)
- opam hitting download limits? (8 messages, latest: Sep 19 2022 at 18:03)
- make test-suite depends on installation? (2 messages, latest: Sep 19 2022 at 07:48)
- Unify local + global context (3 messages, latest: Sep 17 2022 at 18:30)
- Help porting plugin from 8.14 to master (23 messages, latest: Sep 16 2022 at 15:21)
- reduction in the kernel (20 messages, latest: Sep 16 2022 at 13:31)
- Running single test with Dune (8 messages, latest: Sep 15 2022 at 20:43)
- macOS Notarization by INRIA (6 messages, latest: Sep 14 2022 at 12:27)
- Discharging proof states (3 messages, latest: Sep 12 2022 at 12:12)
- Can't find file on loadpath (opam) (6 messages, latest: Sep 07 2022 at 17:09)
- pattern_of_constr on primitive projections (5 messages, latest: Sep 07 2022 at 15:10)
- How to install Coq 8.16.0? (11 messages, latest: Sep 07 2022 at 12:21)
- Backtrace on anomalies (13 messages, latest: Sep 06 2022 at 14:01)
- toplevel exception protections (3 messages, latest: Sep 06 2022 at 07:58)
- 8.16+rc1 is now public (86 messages, latest: Sep 05 2022 at 11:18)
- Test-suite timeout in the CI (22 messages, latest: Sep 01 2022 at 18:43)
- Performance (87 messages, latest: Sep 01 2022 at 14:19)
- Protecting branch creation (5 messages, latest: Sep 01 2022 at 13:44)
- Refman as Zenodo artifact (12 messages, latest: Aug 28 2022 at 10:46)
- cClosure functions (5 messages, latest: Aug 28 2022 at 03:39)
- refman licensing (22 messages, latest: Aug 27 2022 at 20:17)
- breaking change section in changelog (9 messages, latest: Aug 24 2022 at 17:42)
- latex1 test from test-suite fails (5 messages, latest: Aug 24 2022 at 07:17)
- Controlling reduction / annotated casts (10 messages, latest: Aug 22 2022 at 12:03)
- jasmin failing in CI (9 messages, latest: Aug 17 2022 at 14:24)
- ✔ Stack overflow during positivity checking (?) (6 messages, latest: Aug 17 2022 at 12:48)
- 8.16 macOS: findlib issues with Mac installer (3 messages, latest: Aug 16 2022 at 07:53)
- Printing keywords (16 messages, latest: Aug 09 2022 at 13:58)
- Coq Interval master does not build with Coq 8.16+rc1 (13 messages, latest: Aug 08 2022 at 10:05)
- Advice regarding extraction to rust (6 messages, latest: Aug 08 2022 at 05:32)
- Struggling to understand Pp boxes (3 messages, latest: Aug 06 2022 at 23:47)
- Performance Puzzles (7 messages, latest: Aug 06 2022 at 17:14)
- Documentation for Miniml.ml ? (14 messages, latest: Aug 05 2022 at 07:52)
- help debugging Ltac performance? (12 messages, latest: Jul 30 2022 at 16:52)
- Make hint locality warning an error (188 messages, latest: Jul 30 2022 at 16:51)
- ✔ Executable using Ltac_plugin (4 messages, latest: Jul 30 2022 at 15:03)
- tactic popularity contest (1 message, latest: Jul 27 2022 at 22:10)
- Getting statistics about CI time (3 messages, latest: Jul 27 2022 at 16:04)
- Adding support for `./configure -h` to the v8.0 branch? (1 message, latest: Jul 27 2022 at 03:46)
- issue reporting statistics (20 messages, latest: Jul 25 2022 at 15:19)
- Location of errors (regression/change 8.15 (7 messages, latest: Jul 20 2022 at 15:41)
- Warning for deprecated subclass instances (7 messages, latest: Jul 20 2022 at 09:38)
- Universe levels in inductive arity (2 messages, latest: Jul 18 2022 at 10:21)
- ✔ Findlib error with master + nix (3 messages, latest: Jul 12 2022 at 20:31)
- ✔ coq-menhirlib (9 messages, latest: Jul 08 2022 at 13:51)
- ✔ Plugins and coq versions (26 messages, latest: Jul 08 2022 at 07:51)
- CoqIDE package built with Dune (16 messages, latest: Jul 06 2022 at 18:07)
- ✔ Running coqtop without stdlib (9 messages, latest: Jul 05 2022 at 15:23)
- Duplicate universes when declaring constans (24 messages, latest: Jul 04 2022 at 13:57)
- Packaging Coq built with Dune (19 messages, latest: Jul 04 2022 at 13:34)
- Kevin Buzzard interview about Lean (1 message, latest: Jul 01 2022 at 17:56)
- Annotation of hint commands with locality attributes (64 messages, latest: Jul 01 2022 at 09:35)
- Big Dune PR incoming (141 messages, latest: Jun 29 2022 at 13:52)
- docker-keeper must be updated to 0.8.20 (1 message, latest: Jun 29 2022 at 07:36)
- Standalone deps in CI (28 messages, latest: Jun 28 2022 at 10:38)
- Folder access warnings with snap (3 messages, latest: Jun 24 2022 at 20:29)
- add bonak to CI? (15 messages, latest: Jun 24 2022 at 18:59)
- CI artifact use (25 messages, latest: Jun 24 2022 at 07:45)
- Backporting #15271 (14 messages, latest: Jun 23 2022 at 20:28)
- Plugin depending on OCaml library (19 messages, latest: Jun 22 2022 at 06:02)
- Coq Working Group June 2022 (61 messages, latest: Jun 16 2022 at 08:06)
- Named v.s. Unnamed universe levels (14 messages, latest: Jun 14 2022 at 09:23)
- ✔ configure script not doing anything (12 messages, latest: Jun 13 2022 at 11:21)
- Stack overflow in bench (13 messages, latest: Jun 09 2022 at 18:38)
- Locality for Declare ML Module (4 messages, latest: Jun 08 2022 at 20:12)
- Performance of coqchk on instantiated functors (30 messages, latest: Jun 07 2022 at 14:03)
- Auxiliary files (4 messages, latest: Jun 07 2022 at 06:28)
- 8.16 changelog doesn't look right (5 messages, latest: Jun 05 2022 at 09:22)
- Confusing results with coqdep (32 messages, latest: Jun 03 2022 at 19:06)
- Positivity checker and constructors (13 messages, latest: Jun 03 2022 at 04:19)
- Coq installation instructions with opam (2 messages, latest: Jun 02 2022 at 12:59)
- Mutable data structures and concurrency (5 messages, latest: Jun 02 2022 at 12:32)
- GitLab mirroring (3 messages, latest: Jun 02 2022 at 09:06)
- RC vs release notes (8 messages, latest: Jun 01 2022 at 12:35)
- Dead "code" detection / GC of unused definitions (13 messages, latest: May 31 2022 at 16:40)
- ocamldebug on newer ocaml (19 messages, latest: May 31 2022 at 06:45)
- ✔ Weird error with documentation index script (7 messages, latest: May 30 2022 at 10:11)
- Close as not planned. (3 messages, latest: May 28 2022 at 10:23)
- STM woes (66 messages, latest: May 25 2022 at 21:27)
- Roadmap to "consolidation PR" (115 messages, latest: May 25 2022 at 16:16)
- CI for base+async timing out (48 messages, latest: May 25 2022 at 09:59)
- Extraction (5 messages, latest: May 25 2022 at 09:38)
- Outdated release doc (9 messages, latest: May 25 2022 at 07:02)
- SSR breaks parser? (8 messages, latest: May 24 2022 at 22:08)
- Plugins and theories in same package? (43 messages, latest: May 23 2022 at 16:55)
- 4.14 (32 messages, latest: May 23 2022 at 14:02)
- universe inconsistency in coqchk (8 messages, latest: May 22 2022 at 14:13)
- Well-bracketing of Proof-Qed blocks (86 messages, latest: May 21 2022 at 08:03)
- nia failing with segfault on 8.16 async (9 messages, latest: May 19 2022 at 12:27)
- Test-suite on windows (16 messages, latest: May 19 2022 at 08:01)
- Bench for native compute (7 messages, latest: May 18 2022 at 14:00)
- compcert failing in bench? (27 messages, latest: May 18 2022 at 10:38)
- 8.16 branch (7 messages, latest: May 17 2022 at 18:58)
- Better coqc (5 messages, latest: May 17 2022 at 17:50)
- assignment (2 messages, latest: May 17 2022 at 11:40)
- What do you get for test-suite/complexity/pretyping.v (3 messages, latest: May 16 2022 at 19:07)
- Error: Unbound module Nativevalues (6 messages, latest: May 14 2022 at 17:46)
- Status of VAR = NAME in _CoqProject? (8 messages, latest: May 13 2022 at 08:07)
- ✔ misc/11170.sh (8 messages, latest: May 12 2022 at 11:32)
- coqdep and plugin META (59 messages, latest: May 11 2022 at 12:04)
- coqchk and COQLIB (4 messages, latest: May 11 2022 at 11:48)
- coqdep fails on import cats (3 messages, latest: May 10 2022 at 16:42)
- [disc] Make hint locality warning an error (40 messages, latest: May 10 2022 at 08:16)
- ✔ findlib finding coq-core/META from another opam switch (12 messages, latest: May 10 2022 at 06:56)
- >= 4.09 and opam (43 messages, latest: May 09 2022 at 20:53)
- CI elpi broken (7 messages, latest: May 09 2022 at 17:21)
- ✔ OCaml 4.14 for older coq (4 messages, latest: May 09 2022 at 10:19)
- coqdep anomaly on trivial error (5 messages, latest: May 09 2022 at 10:18)
- ci (2 messages, latest: May 07 2022 at 18:16)
- Plugin enter proof mode? (5 messages, latest: May 06 2022 at 15:39)
- opam archive CI caching error (4 messages, latest: May 03 2022 at 10:38)
- GC performance on OCaml 4.14 (41 messages, latest: May 02 2022 at 16:04)
- CI problems (230 messages, latest: May 02 2022 at 11:17)
- CI policy after full Dune switch (29 messages, latest: Apr 29 2022 at 15:46)
- Fatal error: Cannot find file "dllcrt2.o" (6 messages, latest: Apr 29 2022 at 11:53)
- CI Windows (2 messages, latest: Apr 29 2022 at 09:18)
- CI - flocq3/flocq4 (35 messages, latest: Apr 29 2022 at 08:14)
- coqdep supporting `From ... Require ...` (3 messages, latest: Apr 27 2022 at 18:28)
- arrays vs lists (28 messages, latest: Apr 27 2022 at 14:44)
- 4.09 bump (4 messages, latest: Apr 25 2022 at 14:45)
- Error: The file /root/.opamcache/4.13.0+flambda/lib/ocaml/un (2 messages, latest: Apr 25 2022 at 13:44)
- Why do we use -rectypes? (60 messages, latest: Apr 25 2022 at 13:44)
- Canonical projections on `:=` record fields (44 messages, latest: Apr 22 2022 at 07:51)
- Documenting Platform packages (1 message, latest: Apr 21 2022 at 16:33)
- single RM (13 messages, latest: Apr 21 2022 at 14:39)
- Anomalies raised by plugins (51 messages, latest: Apr 19 2022 at 19:40)
- Coq, TCE, logic_monad.v and ARM (13 messages, latest: Apr 18 2022 at 14:06)
- ✔ Compiled library elpi.elpi (in file /usr/lib/ocaml/coq/... (20 messages, latest: Apr 17 2022 at 12:01)
- ✔ Getting coqtop.byte working (6 messages, latest: Apr 16 2022 at 16:53)
- difference between `;` and `.` (44 messages, latest: Apr 14 2022 at 17:20)
- envvar for micromega cache (53 messages, latest: Apr 14 2022 at 15:10)
- GitLab ci connection issue (3 messages, latest: Apr 14 2022 at 12:12)
- stream events (10 messages, latest: Apr 13 2022 at 11:44)
- ✔ Plugins with shared code (32 messages, latest: Apr 11 2022 at 13:37)
- When to group vernac command extend? (5 messages, latest: Apr 09 2022 at 21:55)
- holidays (24 messages, latest: Apr 08 2022 at 20:52)
- Build maintainer team (2 messages, latest: Apr 08 2022 at 16:59)
- Section trickery (4 messages, latest: Apr 07 2022 at 09:18)
- Coqdep slow (93 messages, latest: Apr 07 2022 at 05:37)
- coqchk in test-suite/bugs/ (16 messages, latest: Apr 06 2022 at 21:03)
- Tag for 8.15.1 (3 messages, latest: Apr 06 2022 at 20:11)
- coqbot should mention stale CI (20 messages, latest: Apr 05 2022 at 12:20)
- runners (2 messages, latest: Apr 05 2022 at 11:03)
- Libobject roles (8 messages, latest: Apr 04 2022 at 19:18)
- fixing jasmin (41 messages, latest: Apr 04 2022 at 18:54)
- Contact équipe galinette (10 messages, latest: Apr 04 2022 at 08:49)
- `@coqbot bench` (gitlab stuff) (34 messages, latest: Apr 01 2022 at 22:55)
- -indices-matter changing eliminator of eq (47 messages, latest: Apr 01 2022 at 19:15)
- Why do we have command line typing options? (14 messages, latest: Apr 01 2022 at 16:57)
- `@coqbot bench` (63 messages, latest: Apr 01 2022 at 14:23)
- 8.15.1 release (71 messages, latest: Apr 01 2022 at 11:39)
- building Coq on Windows via opam? (5 messages, latest: Apr 01 2022 at 06:17)
- Docker images from coq-community (6 messages, latest: Apr 01 2022 at 01:43)
- coqchk OOM (23 messages, latest: Mar 31 2022 at 20:45)
- Coq + Windows Working Group (5 messages, latest: Mar 31 2022 at 17:14)
- DELETE_ON_ERROR flipped logic (5 messages, latest: Mar 31 2022 at 14:48)
- CI / refman artifact (11 messages, latest: Mar 30 2022 at 20:52)
- Spring working goup (16 messages, latest: Mar 30 2022 at 17:19)
- coq doc build failure (6 messages, latest: Mar 30 2022 at 14:04)
- dockerfile i386 (5 messages, latest: Mar 29 2022 at 17:07)
- intuition and auto-star (24 messages, latest: Mar 29 2022 at 13:31)
- coqdoc and binder index (7 messages, latest: Mar 28 2022 at 17:16)
- `Admitted` slow (6 messages, latest: Mar 28 2022 at 10:34)
- Admitted used variables (3 messages, latest: Mar 28 2022 at 09:32)
- Minimization noise (27 messages, latest: Mar 26 2022 at 02:58)
- GitHub actions for PRs broken (5 messages, latest: Mar 25 2022 at 15:13)
- TC search best_effort returning invalid results (3 messages, latest: Mar 25 2022 at 13:13)
- windows failing? (41 messages, latest: Mar 23 2022 at 19:06)
- ✔ Effect of `Require` on already loaded lib (6 messages, latest: Mar 23 2022 at 09:06)
- ✔ Non fatal warning in default target (59 messages, latest: Mar 23 2022 at 09:05)
- Where is the MacOS version in Coq 8.14+? (4 messages, latest: Mar 22 2022 at 18:43)
- ci.inria.fr access (1 message, latest: Mar 22 2022 at 14:27)
- Security of bench (52 messages, latest: Mar 22 2022 at 06:48)
- ✔ cannot create regular file '.csdp.cache': Permission de... (67 messages, latest: Mar 21 2022 at 17:36)
- Unsoundness with module subtyping and Prop-squashing (23 messages, latest: Mar 21 2022 at 09:47)
- Pass flags to coqc (72 messages, latest: Mar 20 2022 at 19:43)
- Release 8.16 (29 messages, latest: Mar 19 2022 at 09:44)
- Coq & why3 Debian packaging (62 messages, latest: Mar 18 2022 at 10:56)
- case quiz (11 messages, latest: Mar 17 2022 at 13:57)
- deprecation for definitions (23 messages, latest: Mar 16 2022 at 18:35)
- web public streams (1 message, latest: Mar 16 2022 at 15:56)
- Benchmark noise model (7 messages, latest: Mar 16 2022 at 12:39)
- proofassistants.stackexchange.com (2 messages, latest: Mar 16 2022 at 08:59)
- Snap packages (6 messages, latest: Mar 16 2022 at 06:43)
- econstr version of constr_expr (18 messages, latest: Mar 15 2022 at 17:37)
- Printing in parsing vs execution (20 messages, latest: Mar 14 2022 at 17:02)
- Looking for reviewer for AAC Tactics universe fix (22 messages, latest: Mar 14 2022 at 15:55)
- Quizz on modules (36 messages, latest: Mar 12 2022 at 07:50)
- Help with module code refactoring (17 messages, latest: Mar 11 2022 at 18:53)
- Extended CI Runners (161 messages, latest: Mar 11 2022 at 09:52)
- Proof workers, thread workers, global make pools, ... (29 messages, latest: Mar 11 2022 at 08:55)
- Interlacing of bench results (10 messages, latest: Mar 10 2022 at 20:52)
- Very slow algorithmic in Ssreflect rewrite (41 messages, latest: Mar 10 2022 at 20:29)
- Splitting CoqIDE (301 messages, latest: Mar 10 2022 at 16:46)
- How to reuse OCaml script stuff (75 messages, latest: Mar 10 2022 at 13:28)
- CoqIDE configuration recently broken? (17 messages, latest: Mar 10 2022 at 09:43)
- Options to coqidetop in VSCoq (23 messages, latest: Mar 09 2022 at 22:21)
- Splitting CoqIDE - speed regression (88 messages, latest: Mar 09 2022 at 18:16)
- Gensym in kernel for MBIds (3 messages, latest: Mar 08 2022 at 15:36)
- vscoqtop language server (8 messages, latest: Mar 07 2022 at 08:42)
- Man pages / argument parsing (90 messages, latest: Mar 07 2022 at 06:34)
- Use of kernel names in tactic notations (9 messages, latest: Mar 06 2022 at 23:34)
- Working Group on CEP62/CEP63 (22 messages, latest: Mar 04 2022 at 08:51)
- test-suite + dune (89 messages, latest: Mar 02 2022 at 16:47)
- Minisys and coqdep (10 messages, latest: Mar 02 2022 at 15:35)
- Opaque constants (51 messages, latest: Mar 01 2022 at 20:14)
- ✔ Gitter archive (8 messages, latest: Mar 01 2022 at 18:09)
- opam archive CI not reporting status to GitHub (1 message, latest: Feb 28 2022 at 14:55)
- coq_makefile broken on Windows (1 message, latest: Feb 24 2022 at 15:33)
- Different proof editing example (20 messages, latest: Feb 23 2022 at 16:49)
- ✔ Proofview.Goal.enter_one not triggering (22 messages, latest: Feb 23 2022 at 10:47)
- coq.dev package fails to build (13 messages, latest: Feb 22 2022 at 19:38)
- .mllib? (4 messages, latest: Feb 22 2022 at 12:40)
- coqide dev opam package broken (8 messages, latest: Feb 21 2022 at 20:19)
- ✔ target to build coqtop (7 messages, latest: Feb 18 2022 at 13:11)
- ✔ How to use Top_printers (6 messages, latest: Feb 17 2022 at 22:03)
- debugging coqchk (5 messages, latest: Feb 17 2022 at 17:15)
- hnf and simpl never (9 messages, latest: Feb 17 2022 at 16:19)
- ocaml versions and coq (8 messages, latest: Feb 16 2022 at 21:25)
- refined github (3 messages, latest: Feb 16 2022 at 18:16)
- History for coqtop (9 messages, latest: Feb 16 2022 at 12:31)
- ✔ Weird universe printing due to variance (7 messages, latest: Feb 16 2022 at 09:02)
- pr #15645 https://github.com/coq/coq/pull/15645 (15 messages, latest: Feb 16 2022 at 08:42)
- assignee wanted (3 messages, latest: Feb 15 2022 at 22:33)
- ✔ Explicitly declared universes can not be qualified (4 messages, latest: Feb 14 2022 at 14:09)
- ✔ Make -f Makefile.dune default (4 messages, latest: Feb 14 2022 at 14:09)
- ✔ ocamlfind: Package `coq-core.plugins.ltac' not found (30 messages, latest: Feb 11 2022 at 06:24)
- ✔ findlib errors (4 messages, latest: Feb 11 2022 at 06:22)
- ✔ debugging segfaults (5 messages, latest: Feb 10 2022 at 17:54)
- Scheme duplicate variable names in 8.15 (89 messages, latest: Feb 10 2022 at 10:55)
- make doc_gram (4 messages, latest: Feb 09 2022 at 17:29)
- coqide vs findlib (6 messages, latest: Feb 09 2022 at 13:38)
- Dune and vo files (17 messages, latest: Feb 09 2022 at 10:15)
- How to get `revision` file to update on build (71 messages, latest: Feb 09 2022 at 06:07)
- Combining mutual Fixpoints into a single declaration? (9 messages, latest: Feb 08 2022 at 21:01)
- Dune and Coqdoc (10 messages, latest: Feb 08 2022 at 17:40)
- Help binding Hint Resolve (13 messages, latest: Feb 07 2022 at 15:00)
- Faithful representation of case nodes (16 messages, latest: Feb 06 2022 at 22:36)
- Where is the entry point to coqide? (94 messages, latest: Feb 04 2022 at 17:15)
- coqc scanning PATH (4 messages, latest: Feb 04 2022 at 14:51)
- coq_makefile failure for extra-dev (6 messages, latest: Feb 03 2022 at 16:30)
- Making the Debian packages follow coq's (12 messages, latest: Feb 03 2022 at 12:33)
- ✔ Is -Q recursive? (8 messages, latest: Feb 03 2022 at 09:39)
- Coq Docker rate limit (25 messages, latest: Feb 02 2022 at 18:11)
- Script for automatically addressing Coq warnings (14 messages, latest: Feb 02 2022 at 15:52)
- Why `coqorg/coq:dev` FTBFS currently? (3 messages, latest: Feb 02 2022 at 01:20)
- CI updates for the dune build (8 messages, latest: Feb 01 2022 at 17:30)
- API to know the current file name (4 messages, latest: Feb 01 2022 at 16:42)
- Coq Hackathon February 2022 (81 messages, latest: Jan 31 2022 at 13:11)
- Google Summer of Code 2022 (4 messages, latest: Jan 28 2022 at 14:07)
- Scheme Equality (73 messages, latest: Jan 27 2022 at 16:58)
- Record `{| f := t |}` syntax (8 messages, latest: Jan 27 2022 at 15:46)
- bugs in `match` (10 messages, latest: Jan 26 2022 at 23:47)
- How to better document tactics? (35 messages, latest: Jan 26 2022 at 16:47)
- macOS CI (29 messages, latest: Jan 26 2022 at 10:01)
- ./configure -local no longer exists, what to use now? (7 messages, latest: Jan 26 2022 at 09:46)
- citation? (2 messages, latest: Jan 26 2022 at 09:41)
- ✔ Why doesn't lint job show locations? (7 messages, latest: Jan 25 2022 at 19:55)
- ✔ Where does /usr/bin/coqide come from? (9 messages, latest: Jan 25 2022 at 16:19)
- performance of the category_theory dev (18 messages, latest: Jan 25 2022 at 10:48)
- Files installed in strange location (6 messages, latest: Jan 24 2022 at 21:10)
- Is `Printing Existential Instances` broken? (6 messages, latest: Jan 24 2022 at 15:03)
- Universe incompatibility from MetaCoq and Iris (13 messages, latest: Jan 24 2022 at 12:09)
- fine-grained coq bench (7 messages, latest: Jan 23 2022 at 21:06)
- Weird git hub tar ball issue (14 messages, latest: Jan 22 2022 at 12:07)
- Name binding behavior in Ltac (5 messages, latest: Jan 20 2022 at 21:41)
- pattern_of_constr (1 message, latest: Jan 20 2022 at 20:57)
- Windows CI (110 messages, latest: Jan 19 2022 at 15:16)
- CI Broken? (3 messages, latest: Jan 19 2022 at 13:47)
- Skipped jobs on CI (6 messages, latest: Jan 19 2022 at 13:01)
- Makefile.build/common (5 messages, latest: Jan 17 2022 at 16:51)
- opam package for 8.15.0 (99 messages, latest: Jan 16 2022 at 19:50)
- bench job configuration (3 messages, latest: Jan 14 2022 at 16:08)
- bedrock failing (9 messages, latest: Jan 14 2022 at 14:05)
- 8.14 release thread (76 messages, latest: Jan 13 2022 at 18:42)
- `Retyping.relevance_of_type` on unbound `Rel`s (39 messages, latest: Jan 13 2022 at 11:48)
- The writing is on the wall (114 messages, latest: Jan 11 2022 at 19:29)
- Bug squashing party (6 messages, latest: Jan 10 2022 at 22:38)
- Fixpoints non-wellfounded in erasable subterms accepted (31 messages, latest: Jan 10 2022 at 09:26)
- Dune install: ocaml libs vs coq libs (50 messages, latest: Jan 09 2022 at 14:23)
- Spring cleanup of the evar_map (23 messages, latest: Jan 06 2022 at 20:14)
- odd vs. Odd (23 messages, latest: Dec 29 2021 at 21:16)
- Inlining data in Δ-resolver (8 messages, latest: Dec 29 2021 at 08:37)
- Small naming question: subst_mps (1 message, latest: Dec 27 2021 at 10:48)
- Constant/MutInd API (6 messages, latest: Dec 21 2021 at 09:20)
- How to link other projects in ci (28 messages, latest: Dec 18 2021 at 20:46)
- CI rerunning install step (3 messages, latest: Dec 17 2021 at 21:12)
- opam archive CI cache errors (29 messages, latest: Dec 17 2021 at 11:18)
- Coq 8.15 RC1 (77 messages, latest: Dec 17 2021 at 10:01)
- opam archive CI dune error (35 messages, latest: Dec 16 2021 at 20:51)
- Universe levels and section discharge (5 messages, latest: Dec 15 2021 at 16:27)
- Parsing / execution separation (317 messages, latest: Dec 15 2021 at 14:35)
- coq-serapi versioning (1 message, latest: Dec 15 2021 at 08:40)
- Testing that an error is not an anomaly (11 messages, latest: Dec 14 2021 at 16:16)
- Splitting notation.ml (4 messages, latest: Dec 13 2021 at 13:41)
- [stdlib] Naming convention for moving from Prop to Type (9 messages, latest: Dec 10 2021 at 19:32)
- Backtraces in CoqIDE (6 messages, latest: Dec 10 2021 at 16:43)
- Include libobject (65 messages, latest: Dec 09 2021 at 13:37)
- Bumping dune version (5 messages, latest: Dec 08 2021 at 20:28)
- Bignums maintenance (34 messages, latest: Dec 08 2021 at 18:00)
- Coq 8.14.1 changelog (35 messages, latest: Dec 08 2021 at 13:17)
- Bench plotter (6 messages, latest: Dec 06 2021 at 12:28)
- ci job for the refman (21 messages, latest: Dec 03 2021 at 13:53)
- Hour of Code and education week (60 messages, latest: Dec 03 2021 at 09:45)
- M1 performance (56 messages, latest: Dec 03 2021 at 00:41)
- stale? (4 messages, latest: Dec 02 2021 at 16:17)
- expand_path_macros (15 messages, latest: Dec 02 2021 at 13:11)
- Change in installed files? (1 message, latest: Dec 02 2021 at 02:10)
- gramlib and ocaml-lsp (13 messages, latest: Nov 30 2021 at 19:28)
- ml or mli only? (12 messages, latest: Nov 30 2021 at 19:12)
- Debugging an infinite loop in `interp_constr_may_eval` (5 messages, latest: Nov 30 2021 at 08:06)
- Testing ocaml output in test-suite (3 messages, latest: Nov 30 2021 at 05:21)
- Dynlink module already loaded (4 messages, latest: Nov 29 2021 at 19:07)
- quickchick (11 messages, latest: Nov 29 2021 at 13:51)
- Weird CI error w.r.t. warnings (25 messages, latest: Nov 29 2021 at 13:41)
- coqbot (8 messages, latest: Nov 26 2021 at 17:39)
- plugin in Coq's CI which builds using dune (6 messages, latest: Nov 25 2021 at 16:13)
- Makefile.build? (16 messages, latest: Nov 25 2021 at 14:28)
- vst broken in CI (6 messages, latest: Nov 23 2021 at 18:43)
- Scrolling behaviour in messages window (5 messages, latest: Nov 23 2021 at 17:33)
- tauto plugin (13 messages, latest: Nov 22 2021 at 15:05)
- Canonical vs User map (5 messages, latest: Nov 18 2021 at 12:51)
- flags to control TC search (2 messages, latest: Nov 15 2021 at 12:43)
- Tactic backtrace (6 messages, latest: Nov 15 2021 at 12:32)
- Debian packaging of Coq using Dune (27 messages, latest: Nov 15 2021 at 12:29)
- ✔ Are static libraries really unstripped? (9 messages, latest: Nov 13 2021 at 22:22)
- Closing of known issues (18 messages, latest: Nov 13 2021 at 11:42)
- Taking over maintenance of the Debian package (224 messages, latest: Nov 13 2021 at 11:41)
- Abort for modules/program? (17 messages, latest: Nov 12 2021 at 14:24)
- Deprecating legacy dev workflow (106 messages, latest: Nov 11 2021 at 16:08)
- opam upgrade in the Coq Platform (1 message, latest: Nov 11 2021 at 15:42)
- Tests giving different result on CI and local build (6 messages, latest: Nov 10 2021 at 16:55)
- Flocq broken on master (68 messages, latest: Nov 10 2021 at 15:31)
- ✔ Setting backtrace within coq (10 messages, latest: Nov 10 2021 at 14:29)
- ✔ "kind: feature request" tag (6 messages, latest: Nov 10 2021 at 13:08)
- metacoq ci (6 messages, latest: Nov 10 2021 at 09:01)
- ✔ Problem with local build of ci projects with ml code (11 messages, latest: Nov 09 2021 at 12:03)
- Why are native arrays universe polymorphic? (15 messages, latest: Nov 08 2021 at 16:31)
- Debian package of Coq Platform (11 messages, latest: Nov 08 2021 at 16:20)
- Coq ecosystem licensing (12 messages, latest: Nov 08 2021 at 10:17)
- Change of manual license for DFSG compatibility (15 messages, latest: Nov 06 2021 at 15:20)
- Weird test-suite failure (14 messages, latest: Nov 06 2021 at 14:27)
- dune build spending its time running coqdep (78 messages, latest: Nov 05 2021 at 19:41)
- ✔ gitlab.inria.fr account? (24 messages, latest: Nov 04 2021 at 09:33)
- OCaml's new Epheremron API (2 messages, latest: Nov 03 2021 at 17:16)
- opam update fails (7 messages, latest: Nov 03 2021 at 15:57)
- adding Stalmarck to Coq CI (5 messages, latest: Nov 02 2021 at 08:58)
- exact_no_check, repeated casts in proof terms (20 messages, latest: Nov 01 2021 at 16:40)
- ✔ Generating match expression with nested patterns (7 messages, latest: Oct 31 2021 at 20:53)
- SProp, pose and change (6 messages, latest: Oct 29 2021 at 11:47)
- master broken (7 messages, latest: Oct 28 2021 at 13:28)
- coq_tools failing in CI (1 message, latest: Oct 27 2021 at 12:11)
- CI failing (82 messages, latest: Oct 27 2021 at 08:20)
- Gappa overlays (3 messages, latest: Oct 26 2021 at 21:18)
- Type of a Global (13 messages, latest: Oct 25 2021 at 15:39)
- pkg:nix:deploy unhappy (7 messages, latest: Oct 23 2021 at 11:37)
- CI issues downloading from https://coq.inria.fr/opam (2 messages, latest: Oct 23 2021 at 11:23)
- ✔ fcsl_pcm broken (9 messages, latest: Oct 22 2021 at 11:35)
- OPAM packages and Dune (19 messages, latest: Oct 21 2021 at 13:26)
- New github projects (4 messages, latest: Oct 21 2021 at 13:19)
- Coq Website (54 messages, latest: Oct 20 2021 at 13:53)
- wiki spam (9 messages, latest: Oct 20 2021 at 10:24)
- pendulum broken (1 message, latest: Oct 19 2021 at 18:30)
- Implementation of CI scripts (9 messages, latest: Oct 16 2021 at 12:21)
- non team codeowners (3 messages, latest: Oct 15 2021 at 14:23)
- kind: wish (7 messages, latest: Oct 15 2021 at 12:54)
- coq.inria.fr down? (4 messages, latest: Oct 13 2021 at 08:33)
- The future of futures (1 message, latest: Oct 12 2021 at 11:59)
- release process (2 messages, latest: Oct 11 2021 at 11:35)
- Puzzling error (7 messages, latest: Oct 08 2021 at 13:04)
- Directory handling code in coqdep (29 messages, latest: Oct 08 2021 at 10:35)
- regression in graph-theory related to HB (1 message, latest: Oct 04 2021 at 07:56)
- Interpretation of ci-basic_overlay.sh (3 messages, latest: Oct 02 2021 at 11:37)
- Coq sponsoring banner (14 messages, latest: Sep 30 2021 at 19:25)
- Future of Prop, SProp and Type (33 messages, latest: Sep 29 2021 at 15:41)
- whd_nored? (3 messages, latest: Sep 29 2021 at 15:15)
- Building via coq_makefile running into missing-mli error (17 messages, latest: Sep 29 2021 at 12:13)
- Installing coq.dev through opam, missing binaries (31 messages, latest: Sep 28 2021 at 18:15)
- Windows CI: cygwin repo server down again (3 messages, latest: Sep 28 2021 at 15:40)
- Average bench results (2 messages, latest: Sep 28 2021 at 14:52)
- STM and summary (112 messages, latest: Sep 26 2021 at 18:50)
- coqbot closing PRs (23 messages, latest: Sep 24 2021 at 15:58)
- Platform tagging for 8.14 (13 messages, latest: Sep 23 2021 at 17:32)
- coq_makefile and `-devel` (post dune) (13 messages, latest: Sep 23 2021 at 12:40)
- Using known parameters to type arguments of a constructor (4 messages, latest: Sep 22 2021 at 14:54)
- What is ne_reference_list (2 messages, latest: Sep 20 2021 at 13:54)
- Coq 8.14 new timeline (2 messages, latest: Sep 20 2021 at 13:21)
- www PR conventions (3 messages, latest: Sep 19 2021 at 13:34)
- Release candidate version naming breaks PG (3 messages, latest: Sep 19 2021 at 10:35)
- bignums test breakage (2 messages, latest: Sep 18 2021 at 08:41)
- Coq Platform Windows CI broken cause SF changed its URLs (19 messages, latest: Sep 17 2021 at 14:34)
- configure arguments (9 messages, latest: Sep 17 2021 at 11:37)
- restriction of one associativity per level? (12 messages, latest: Sep 16 2021 at 18:52)
- LSP server status? (8 messages, latest: Sep 16 2021 at 14:40)
- Installing plugin requires -R ? (6 messages, latest: Sep 14 2021 at 15:51)
- Noise in CI logs (4 messages, latest: Sep 14 2021 at 15:22)
- odoc complaints (4 messages, latest: Sep 14 2021 at 10:58)
- simpl never and hnf (4 messages, latest: Sep 11 2021 at 00:32)
- reduce_to_ind_gen hnf? (3 messages, latest: Sep 10 2021 at 13:49)
- Github dev (3 messages, latest: Sep 10 2021 at 09:34)
- CoqIDE "coqtop died badly" with Coq 8.14 dev (41 messages, latest: Sep 09 2021 at 16:59)
- Naming evars produced by setoid rewrite (2 messages, latest: Sep 08 2021 at 15:05)
- Building with Dune (5 messages, latest: Sep 08 2021 at 06:55)
- Mtac2 broken in Coq's CI (14 messages, latest: Sep 07 2021 at 19:53)
- async failures (3 messages, latest: Sep 07 2021 at 12:53)
- fun charts (2 messages, latest: Sep 07 2021 at 11:40)
- Basic API for functions about terms, contexts, substitutions (2 messages, latest: Sep 03 2021 at 10:37)
- Primitive Projections (7 messages, latest: Sep 02 2021 at 21:08)
- coq-core and coq-stdlib opam packages (21 messages, latest: Aug 30 2021 at 18:55)
- Cachix not pulling precompiled Coq master (7 messages, latest: Aug 29 2021 at 11:51)
- Joining @coq/pushers (8 messages, latest: Aug 28 2021 at 19:47)
- Backporting policy (39 messages, latest: Aug 28 2021 at 17:20)
- Status of retroknowledge in module types (3 messages, latest: Aug 28 2021 at 13:41)
- Resuming Coq calls (4 messages, latest: Aug 27 2021 at 09:56)
- Plugin Tutorial (14 messages, latest: Aug 26 2021 at 15:57)
- interactive configure? (11 messages, latest: Aug 25 2021 at 12:23)
- moving constructor in "new" proof engine and to evarconv (4 messages, latest: Aug 23 2021 at 12:39)
- fold_left on maps in CMap (1 message, latest: Aug 23 2021 at 12:13)
- Invertible constructor (7 messages, latest: Aug 23 2021 at 10:10)
- vacances (1 message, latest: Aug 21 2021 at 07:20)
- Generating "projections" for internal purpose (6 messages, latest: Aug 20 2021 at 16:48)
- mutual_inductive_body API (6 messages, latest: Aug 20 2021 at 16:43)
- Proofview.tclENV: when is it useful? (7 messages, latest: Aug 20 2021 at 16:23)
- Well-foundedness check may fail unexpectedly. (2 messages, latest: Aug 19 2021 at 11:07)
- miniF2F (5 messages, latest: Aug 19 2021 at 01:00)
- How to suggest command in error message (2 messages, latest: Aug 18 2021 at 17:44)
- Dropping end from match in coq (27 messages, latest: Aug 13 2021 at 17:34)
- Automatic re-test of bugs (3 messages, latest: Aug 13 2021 at 17:05)
- ✔ How to pass jobs to test-suite build (12 messages, latest: Aug 12 2021 at 12:30)
- ✔ Test-suite fake_ide issue (9 messages, latest: Aug 12 2021 at 10:23)
- osx CI not happy (4 messages, latest: Aug 09 2021 at 12:16)
- bench runners (2 messages, latest: Aug 09 2021 at 08:47)
- Unification and futile queries after a step of reduction (16 messages, latest: Aug 09 2021 at 07:53)
- bench failing packages (28 messages, latest: Aug 08 2021 at 18:01)
- Intended semantics of `Scheme` command (11 messages, latest: Aug 05 2021 at 05:03)
- On η-expansion in hint matching (17 messages, latest: Jul 31 2021 at 21:26)
- Section discharge (102 messages, latest: Jul 29 2021 at 16:41)
- Why is vst taking so long (16 messages, latest: Jul 29 2021 at 11:27)
- terminology used for universe API (76 messages, latest: Jul 27 2021 at 12:53)
- Primitive Projection mode (66 messages, latest: Jul 26 2021 at 18:52)
- ✔ Best way to get output of dune exec (27 messages, latest: Jul 23 2021 at 18:14)
- Why github actions and coqbot? (4 messages, latest: Jul 23 2021 at 17:36)
- Memory consumption (2 messages, latest: Jul 23 2021 at 13:36)
- Stdlib (8 messages, latest: Jul 23 2021 at 09:18)
- Building with memory limits (20 messages, latest: Jul 22 2021 at 15:24)
- Adding locality to Typeclasses Opaque (94 messages, latest: Jul 22 2021 at 14:46)
- Adding accels in lablgtk (3 messages, latest: Jul 22 2021 at 13:15)
- fiat-parser CI (9 messages, latest: Jul 22 2021 at 00:50)
- Generalizing only over used section polymorphic universes (69 messages, latest: Jul 21 2021 at 10:14)
- if: "Needed cmt file of module 'Hints' (1 message, latest: Jul 20 2021 at 15:24)
- ✔ Add label to not run CI (3 messages, latest: Jul 20 2021 at 12:25)
- no cmx file was found in path for module Zarith_version (19 messages, latest: Jul 19 2021 at 18:12)
- CI failure with bedrock2 (14 messages, latest: Jul 19 2021 at 11:01)
- Building test-suite with dune (3 messages, latest: Jul 15 2021 at 19:38)
- Grammar railroad diagram (5 messages, latest: Jul 15 2021 at 16:48)
- Debugging with `ocamldebug` (43 messages, latest: Jul 15 2021 at 15:37)
- Unbound module Mltop (13 messages, latest: Jul 12 2021 at 15:01)
- Unlabeled issues (27 messages, latest: Jul 10 2021 at 22:44)
- `make unit-tests` not working (7 messages, latest: Jul 09 2021 at 12:32)
- Testing anomaly that becomes error (9 messages, latest: Jul 09 2021 at 12:03)
- GitHub edit button (13 messages, latest: Jul 09 2021 at 10:50)
- Syntax of projections (10 messages, latest: Jul 07 2021 at 13:56)
- Anomaly with Function (1 message, latest: Jul 07 2021 at 12:52)
- What is the reason for the `p.(f)` syntax? (145 messages, latest: Jul 06 2021 at 15:40)
- tauto plugin? (3 messages, latest: Jul 05 2021 at 12:21)
- nativevalues.cmi version mismatch (3 messages, latest: Jul 02 2021 at 20:13)
- bidi vs coercions (2 messages, latest: Jun 30 2021 at 11:53)
- tac-in-terms and shelve (7 messages, latest: Jun 25 2021 at 14:44)
- New Github Issue system (2 messages, latest: Jun 25 2021 at 12:57)
- Bytecode build (20 messages, latest: Jun 23 2021 at 18:32)
- Coq Workshop 2021 (2 messages, latest: Jun 22 2021 at 19:00)
- Pcoq.Rule API and dynamic code (5 messages, latest: Jun 22 2021 at 16:25)
- Local CI (8 messages, latest: Jun 22 2021 at 13:16)
- CI failure with unimath (8 messages, latest: Jun 22 2021 at 13:00)
- CI failure in build:base (17 messages, latest: Jun 21 2021 at 11:58)
- Auto CI Minimization (1 message, latest: Jun 21 2021 at 01:43)
- Windows CI failure cause of gnome mirror unavailable (11 messages, latest: Jun 18 2021 at 15:57)
- opam package split (15 messages, latest: Jun 18 2021 at 06:52)
- coq.dev package (16 messages, latest: Jun 15 2021 at 08:36)
- Weird bench error (6 messages, latest: Jun 12 2021 at 08:33)
- `merge-pr.sh`? (20 messages, latest: Jun 08 2021 at 12:57)
- usr/share/coq-core/texmf/tex/latex/misc/coqdoc.sty (3 messages, latest: Jun 04 2021 at 07:09)
- Becoming member of the libraray maintainer GIT group (7 messages, latest: Jun 02 2021 at 11:54)
- Should my Z lemmas go into the standard library? (6 messages, latest: Jun 02 2021 at 09:01)
- CI artifacts do not prevent CI targets from rebuilding (2 messages, latest: Jun 02 2021 at 01:14)
- Reverse coercions (5 messages, latest: Jun 01 2021 at 11:30)
- CI failure: ci-coq_tools (5 messages, latest: May 28 2021 at 14:31)
- test-suite failure with local-late-extensions (9 messages, latest: May 28 2021 at 13:53)
- native compiler errors (3 messages, latest: May 28 2021 at 00:11)
- LoadPath library organization (3 messages, latest: May 28 2021 at 00:09)
- Is this changelog entry OK? (4 messages, latest: May 27 2021 at 17:53)
- Debugging make ci-mathcomp (13 messages, latest: May 27 2021 at 16:26)
- PR requests rebase, but I am up to date (3 messages, latest: May 26 2021 at 15:34)
- 8.14 deadline and improving `inversion_sigma` (6 messages, latest: May 26 2021 at 07:15)
- CI Minimization (11 messages, latest: May 24 2021 at 00:35)
- Relocating Coq install? (3 messages, latest: May 22 2021 at 12:27)
- LSP (4 messages, latest: May 21 2021 at 18:35)
- sudo broken on Coq CI docker images (4 messages, latest: May 21 2021 at 13:35)
- requesting assignee (6 messages, latest: May 21 2021 at 11:54)
- Multiple PRs involving the same head commit mess with checks (3 messages, latest: May 21 2021 at 10:06)
- Why induction is so slow (34 messages, latest: May 17 2021 at 20:26)
- CoqIDE icons (21 messages, latest: May 17 2021 at 11:12)
- coqbot CI minimize (2 messages, latest: May 17 2021 at 00:31)
- 8.9 Proof.run_tactic getting new context and subgoals (8 messages, latest: May 12 2021 at 19:13)
- docker-coq: heads-up about hardcoded versions in coqorg/base (1 message, latest: May 12 2021 at 00:27)
- Dune Migration (190 messages, latest: May 11 2021 at 21:28)
- git process errors (36 messages, latest: May 10 2021 at 14:56)
- Using dune (409 messages, latest: May 09 2021 at 00:08)
- opam install cannot find directory? (11 messages, latest: May 07 2021 at 23:08)
- stdlib broken on CI (2 messages, latest: May 07 2021 at 21:09)
- Is the test suite slower with dune? (7 messages, latest: May 07 2021 at 16:11)
- coqide shim not working (9 messages, latest: May 07 2021 at 13:13)
- coq-club moderated by default? (1 message, latest: May 06 2021 at 20:34)
- bench broken? (2 messages, latest: May 05 2021 at 17:56)
- UnivSubst and Array (5 messages, latest: May 04 2021 at 12:24)
- C-c on Eval native_compute in (15 messages, latest: May 04 2021 at 00:16)
- make install on Mac (38 messages, latest: May 03 2021 at 12:32)
- Assembler errors on Mac (looks familiar from Cygwin) (1 message, latest: May 02 2021 at 07:33)
- git prw: a command to easily fetch & force-push a PR branch (6 messages, latest: May 01 2021 at 15:23)
- opam source (3 messages, latest: Apr 30 2021 at 18:34)
- Ltac Debugger Protocol (10 messages, latest: Apr 28 2021 at 13:53)
- fiat-crypto currently broken (2 messages, latest: Apr 28 2021 at 12:45)
- coq.dev package broken? (15 messages, latest: Apr 28 2021 at 12:42)
- Documentation discussion in OCaml's discuss (2 messages, latest: Apr 28 2021 at 10:35)
- coqide & dune wrapper (60 messages, latest: Apr 27 2021 at 13:25)
- coq master for HoTT not working (20 messages, latest: Apr 27 2021 at 12:24)
- API to know if we are in a functor (7 messages, latest: Apr 26 2021 at 11:02)
- Reduction tactics stack overflow (5 messages, latest: Apr 21 2021 at 14:43)
- `Time` is inaccurate since Coq 8.5 (24 messages, latest: Apr 20 2021 at 21:41)
- HoTT failing on CI (20 messages, latest: Apr 20 2021 at 08:48)
- Function composition notation (8 messages, latest: Apr 19 2021 at 16:29)
- Changed behavior of reduction tactics. (14 messages, latest: Apr 17 2021 at 15:49)
- structure of opam 'lib' dir (5 messages, latest: Apr 17 2021 at 15:36)
- make refman-html (4 messages, latest: Apr 16 2021 at 10:35)
- macos dmg failure in CI (5 messages, latest: Apr 16 2021 at 10:12)
- coq-club archives no longer public? (2 messages, latest: Apr 16 2021 at 07:24)
- ocaml early bird debugger (5 messages, latest: Apr 14 2021 at 13:41)
- coqc and the ltac debugger (3 messages, latest: Apr 14 2021 at 13:36)
- kind: infrastructure (3 messages, latest: Apr 08 2021 at 14:35)
- windows github action (16 messages, latest: Apr 07 2021 at 20:05)
- Feedback vs CWarnings (5 messages, latest: Apr 07 2021 at 16:48)
- coqc usage (227 messages, latest: Apr 06 2021 at 19:50)
- Coq OCaml API on coq.github.io disappeared (6 messages, latest: Apr 06 2021 at 13:03)
- test-suite (6 messages, latest: Apr 04 2021 at 18:04)
- Mac bytecode: should we switch to -no-custom ? (23 messages, latest: Apr 04 2021 at 14:33)
- Undefined symbols when loading printers (38 messages, latest: Apr 02 2021 at 12:01)
- native compiler bench (21 messages, latest: Apr 01 2021 at 22:24)
- (Γ ⊢ x : T) → (Γ ⊢ T type) (9 messages, latest: Apr 01 2021 at 22:15)
- -set option true/false ===< yes/no? (3 messages, latest: Apr 01 2021 at 19:53)
- release 8.13.2 (1 message, latest: Apr 01 2021 at 14:46)
- Minor Perf Issues in Ltac Debug (5 messages, latest: Apr 01 2021 at 12:46)
- Timing diffs (3 messages, latest: Apr 01 2021 at 12:18)
- CI: MetaCoq is failing (22 messages, latest: Mar 31 2021 at 10:11)
- Induction induction (191 messages, latest: Mar 29 2021 at 14:48)
- SProp breaks subject reduction? (3 messages, latest: Mar 26 2021 at 20:46)
- Binding a tactic in a Hint Extern (93 messages, latest: Mar 25 2021 at 15:45)
- bedrock2 ci broken (8 messages, latest: Mar 25 2021 at 14:40)
- auto-milestoning (10 messages, latest: Mar 25 2021 at 10:21)
- Failing to build ci-mtac2 with Dune (6 messages, latest: Mar 23 2021 at 22:50)
- Creating evars the same way `open_constr` does. (16 messages, latest: Mar 23 2021 at 18:17)
- Warning on implicit hint database declaration (63 messages, latest: Mar 23 2021 at 13:36)
- Debugging Btermdn treatment of variables (6 messages, latest: Mar 22 2021 at 16:40)
- Cryptic Ltac2 function names in `perf` output (27 messages, latest: Mar 19 2021 at 17:59)
- Markdown in issue titles (1 message, latest: Mar 18 2021 at 19:34)
- Deadlock in OCaml runtime (70 messages, latest: Mar 17 2021 at 03:09)
- Decomposing syntactic patterns (1 message, latest: Mar 16 2021 at 11:40)
- Call for feedback: Topic Working Groups (12 messages, latest: Mar 14 2021 at 17:31)
- -no-naked-pointers (5 messages, latest: Mar 13 2021 at 15:16)
- out of memory on paramcoq (4 messages, latest: Mar 12 2021 at 14:23)
- side effects are evil (8 messages, latest: Mar 12 2021 at 13:17)
- Coq-HoTT in the platform? (1 message, latest: Mar 12 2021 at 11:42)
- positivity parametrization? (11 messages, latest: Mar 11 2021 at 09:57)
- paramcoq ci errors (2 messages, latest: Mar 10 2021 at 21:35)
- Docs are unavailable (7 messages, latest: Mar 09 2021 at 15:26)
- output-sync (14 messages, latest: Mar 09 2021 at 13:48)
- coq-core and coq, duplicate libs (9 messages, latest: Mar 08 2021 at 18:31)
- Bench broken (5 messages, latest: Mar 07 2021 at 16:37)
- 8.14 timeline / which milestone to set for merged PRs (4 messages, latest: Mar 06 2021 at 14:16)
- unification instantiates evar incorrectly (34 messages, latest: Mar 03 2021 at 13:53)
- Debugging a Nix problem (38 messages, latest: Mar 02 2021 at 13:58)
- Constructing Notations in OCaml (18 messages, latest: Mar 01 2021 at 11:49)
- ssreflect rewrite problem (5 messages, latest: Feb 27 2021 at 10:04)
- ocaml 4.12 (7 messages, latest: Feb 26 2021 at 17:43)
- Release 8.13.1 (8 messages, latest: Feb 22 2021 at 22:48)
- coqc master seg faults in Coq Platform CI (4 messages, latest: Feb 18 2021 at 10:00)
- paramcoq ci doesn't like native compute? (5 messages, latest: Feb 17 2021 at 18:04)
- CI and perennial (35 messages, latest: Feb 12 2021 at 15:36)
- Vernacular commands and Gallina types (1 message, latest: Feb 11 2021 at 19:33)
- Inductive relative context (5 messages, latest: Feb 11 2021 at 13:46)
- new bench machines (33 messages, latest: Feb 11 2021 at 00:08)
- Finding names used in a term (1 message, latest: Feb 07 2021 at 19:50)
- contribs on the CI (2 messages, latest: Feb 03 2021 at 21:47)
- native_compute on the bench (12 messages, latest: Feb 03 2021 at 13:07)
- Get context after running tactic (11 messages, latest: Feb 02 2021 at 23:45)
- Dynlink error: no implementation available for Tacentries (20 messages, latest: Feb 02 2021 at 23:21)
- Debugging Coq with OCaml 4.11 (30 messages, latest: Feb 02 2021 at 23:17)
- Windows CI might be a bit rough these days (7 messages, latest: Feb 02 2021 at 18:25)
- dependency on num (4 messages, latest: Feb 02 2021 at 18:19)
- review request spam on backport PR (7 messages, latest: Jan 28 2021 at 14:52)
- Warning config as attribute (4 messages, latest: Jan 22 2021 at 14:24)
- fiat-crypto CI broken (5 messages, latest: Jan 20 2021 at 22:51)
- Change of case representation (353 messages, latest: Jan 18 2021 at 17:24)
- infinite loops in type inference? (1 message, latest: Jan 15 2021 at 18:41)
- GitHub adds auto-merge (1 message, latest: Jan 13 2021 at 09:28)
- (Primitive) Projections and local defs in CClosure (whd) (2 messages, latest: Jan 12 2021 at 11:36)
- Vernacstate.Declare.get_current_proof_name (8 messages, latest: Jan 11 2021 at 20:46)
- Libobject: what is "Global universe name state"? (39 messages, latest: Jan 11 2021 at 16:03)
- Incompatible assumptions error after re-compiling Coq 8.13 (18 messages, latest: Jan 10 2021 at 21:08)
- Debugging `Not_found` anomaly in Ltac2 `eval_cbn` (4 messages, latest: Jan 06 2021 at 13:11)
- 8.13 release thread (58 messages, latest: Jan 06 2021 at 11:48)
- build pdf manual (8 messages, latest: Jan 05 2021 at 15:50)
- Async and classification (90 messages, latest: Jan 05 2021 at 09:58)
- Help with building a plugin (11 messages, latest: Dec 29 2020 at 22:05)
- Ltac2 Binder.make (2 messages, latest: Dec 29 2020 at 19:27)
- Dev opam packages for Coq related OCaml packages (gappa, ..) (19 messages, latest: Dec 29 2020 at 14:27)
- Issues building CoqIDE on master (8 messages, latest: Dec 28 2020 at 20:27)
- Debugging CI issue with output redirect (26 messages, latest: Dec 21 2020 at 18:29)
- Jenkins shutdown (2 messages, latest: Dec 21 2020 at 09:52)
- minimal coq make target (67 messages, latest: Dec 18 2020 at 19:18)
- Question from Cuq Club about primitive types and extraction (10 messages, latest: Dec 16 2020 at 18:15)
- no betas for 8.14 and later? (82 messages, latest: Dec 16 2020 at 16:09)
- recent changes to the native compiler? (401 messages, latest: Dec 16 2020 at 16:07)
- `filter_stack_domain` of guard checker using wrong context? (4 messages, latest: Dec 16 2020 at 10:21)
- Help with issue porting a plugin (54 messages, latest: Dec 15 2020 at 13:40)
- Strange CI failure (7 messages, latest: Dec 11 2020 at 18:15)
- Cachix allowance (2 messages, latest: Dec 11 2020 at 14:42)
- OCaml variants in Docker-Coq (33 messages, latest: Dec 10 2020 at 17:06)
- External libraries in a plugin (13 messages, latest: Dec 09 2020 at 16:25)
- WG about namespaces (26 messages, latest: Dec 08 2020 at 16:10)
- Number of TC candidates (1 message, latest: Dec 08 2020 at 10:14)
- Preventing pushing new branches to coq repo (4 messages, latest: Dec 07 2020 at 20:58)
- Homebrew failing on release day RED ALERT (19 messages, latest: Dec 07 2020 at 12:24)
- CAMLDEP hangs on master? (1 message, latest: Dec 04 2020 at 21:01)
- bench failures (9 messages, latest: Dec 03 2020 at 11:54)
- CaseInvert w.r.t. case change of repr (10 messages, latest: Dec 02 2020 at 19:24)
- Printing performance regression from 8.12.1 to master (17 messages, latest: Dec 02 2020 at 15:39)
- module attached locality (1 message, latest: Dec 02 2020 at 13:58)
- Jason's PhD discussion (50 messages, latest: Nov 30 2020 at 20:39)
- CI: OSX installer (54 messages, latest: Nov 29 2020 at 02:12)
- Tagging for the Windows installer (9 messages, latest: Nov 28 2020 at 11:37)
- Benching v8.13 (14 messages, latest: Nov 27 2020 at 16:04)
- bignum (7 messages, latest: Nov 27 2020 at 14:36)
- API to expand a primitive projction (4 messages, latest: Nov 27 2020 at 10:28)
- definitions.rst (3 messages, latest: Nov 26 2020 at 10:58)
- What to do with auto implicit arguments in contexts (1 message, latest: Nov 25 2020 at 19:16)
- Timing options in CoqMakefile (57 messages, latest: Nov 25 2020 at 16:49)
- Ltac2 API to access the constructor and fields of a record (13 messages, latest: Nov 24 2020 at 17:02)
- Plugins with conflicting syntax (6 messages, latest: Nov 24 2020 at 16:44)
- Unsigned vs signed integers (22 messages, latest: Nov 24 2020 at 16:37)
- CoqMakefile environment variables (52 messages, latest: Nov 24 2020 at 13:23)
- change gc during require? (4 messages, latest: Nov 20 2020 at 21:05)
- Changes to unification order in 8.12(.1) (12 messages, latest: Nov 20 2020 at 11:17)
- Bugzilla archive (7 messages, latest: Nov 19 2020 at 15:44)
- commit hook (11 messages, latest: Nov 19 2020 at 11:25)
- Docker limits (5 messages, latest: Nov 18 2020 at 16:20)
- Perennial in CI (37 messages, latest: Nov 17 2020 at 13:55)
- Strange clang error (3 messages, latest: Nov 14 2020 at 14:13)
- 8.12.1 packaging (2 messages, latest: Nov 13 2020 at 23:10)
- lazy linking of constants (1 message, latest: Nov 13 2020 at 18:36)
- Website down? (26 messages, latest: Nov 13 2020 at 09:14)
- Expanding the CI test-suite failures (8 messages, latest: Nov 12 2020 at 14:41)
- moving more files to EConstr (11 messages, latest: Nov 12 2020 at 13:32)
- Iris folder structure changes (8 messages, latest: Nov 12 2020 at 10:35)
- Coq-as-compiler (53 messages, latest: Nov 11 2020 at 18:56)
- coq-idetop for 8.13 (3 messages, latest: Nov 11 2020 at 18:16)
- coq master CI failure in std++ (4 messages, latest: Nov 11 2020 at 14:16)
- Environments at closing time (14 messages, latest: Nov 10 2020 at 16:04)
- 8.12 release thread (440 messages, latest: Nov 10 2020 at 13:27)
- coquelicot failing in ci (5 messages, latest: Nov 05 2020 at 15:40)
- normalization of universes in interactive mutual fixpoints (13 messages, latest: Nov 04 2020 at 17:08)
- Code path in mutual definition (15 messages, latest: Nov 04 2020 at 01:17)
- Asserting an inductive is cumulative (2 messages, latest: Nov 03 2020 at 19:31)
- Algebraic universes in the env (36 messages, latest: Nov 02 2020 at 15:13)
- Extending Ltac2 (4 messages, latest: Oct 30 2020 at 15:44)
- CClosure.whd_stack as a tactic? (13 messages, latest: Oct 30 2020 at 12:53)
- Uninstallable CoqIDE 8.12.0-1 in OPAM (10 messages, latest: Oct 28 2020 at 16:30)
- Release plan for 8.13 (6 messages, latest: Oct 26 2020 at 10:32)
- Pyrolyse (4 messages, latest: Oct 24 2020 at 11:20)
- 3395 (14 messages, latest: Oct 22 2020 at 18:15)
- Qed timing & universes (22 messages, latest: Oct 21 2020 at 18:25)
- Reviews for non-inductive number/string notation PR? (2 messages, latest: Oct 21 2020 at 13:58)
- Nix and native_compute (8 messages, latest: Oct 19 2020 at 10:16)
- quiz (32 messages, latest: Oct 17 2020 at 10:07)
- coqbot merging does not include merger information (10 messages, latest: Oct 15 2020 at 11:04)
- inductive/constructor universe instance (2 messages, latest: Oct 14 2020 at 20:14)
- merlin for gramlib (14 messages, latest: Oct 14 2020 at 19:21)
- Coq/plugin module name clashes (8 messages, latest: Oct 13 2020 at 18:07)
- Building Docker-Coq images more often (27 messages, latest: Oct 12 2020 at 21:15)
- typeops and == (7 messages, latest: Oct 12 2020 at 12:03)
- Bad naming in practice (3 messages, latest: Oct 10 2020 at 11:03)
- Finding differences in identical proof terms (61 messages, latest: Oct 09 2020 at 14:35)
- memtrace (73 messages, latest: Oct 08 2020 at 22:48)
- Anomaly "Signature and its instance do not match" (7 messages, latest: Oct 01 2020 at 09:05)
- Keyword Define as synonym to Proof (15 messages, latest: Sep 30 2020 at 13:23)
- Ocaml version sync between Coq's nix file and CI devs nix (5 messages, latest: Sep 29 2020 at 07:45)
- Failing to compile coq.dev (53 messages, latest: Sep 27 2020 at 19:34)
- clone with --single-branch in CI? (3 messages, latest: Sep 25 2020 at 19:15)
- Verdi bench stuck (5 messages, latest: Sep 25 2020 at 11:17)
- zarith (5 messages, latest: Sep 24 2020 at 23:47)
- Dune beginner question (22 messages, latest: Sep 24 2020 at 19:00)
- Serialization and Restoring of subgoals (25 messages, latest: Sep 23 2020 at 14:48)
- --no-qed-check previous call (2 messages, latest: Sep 23 2020 at 13:56)
- ocamlformat (126 messages, latest: Sep 21 2020 at 21:51)
- CI docker images? (19 messages, latest: Sep 20 2020 at 13:49)
- ocamldebug slow on ocaml 4.11? (20 messages, latest: Sep 18 2020 at 19:14)
- building on debian/ubuntu (6 messages, latest: Sep 18 2020 at 07:25)
- Ocaml 4.07.1 fails to compile with Apple XCode 12 (7 messages, latest: Sep 17 2020 at 14:48)
- Windows CI runner maintenance (12 messages, latest: Sep 16 2020 at 13:43)
- NbE and the implementation of the VM (11 messages, latest: Sep 12 2020 at 08:43)
- AAC Tactics broken on master? (13 messages, latest: Sep 11 2020 at 15:02)
- Pfedit.build_by_tactic (16 messages, latest: Sep 10 2020 at 15:51)
- Citing Coq 8.12 (3 messages, latest: Sep 10 2020 at 08:12)
- Autogenerating test-suite files from CI failures (3 messages, latest: Sep 09 2020 at 17:23)
- Flocq bug report (6 messages, latest: Sep 09 2020 at 08:39)
- Rewrite * (5 messages, latest: Sep 08 2020 at 01:25)
- Verified Kernel (32 messages, latest: Sep 07 2020 at 11:56)
- holiday (3 messages, latest: Sep 07 2020 at 07:28)
- coqbot behaving strangely? (10 messages, latest: Sep 04 2020 at 19:08)
- More machines for benchmarking (13 messages, latest: Sep 02 2020 at 20:28)
- Online alternative to CUDW? (3 messages, latest: Sep 02 2020 at 08:03)
- coq.inria.fr website down? (4 messages, latest: Aug 31 2020 at 15:57)
- ld errors on master (48 messages, latest: Aug 31 2020 at 14:29)
- Strange CI failures (8 messages, latest: Aug 29 2020 at 10:23)
- old issue assignments (3 messages, latest: Aug 28 2020 at 16:01)
- uState performance (3 messages, latest: Aug 28 2020 at 15:18)
- opam archive CI seems dead (1 message, latest: Aug 26 2020 at 18:46)
- coq-rewriter-perf-SuperFast timing (10 messages, latest: Aug 26 2020 at 03:18)
- Why is coqtail failing in ci? (3 messages, latest: Aug 24 2020 at 18:21)
- Bench? (49 messages, latest: Aug 24 2020 at 12:35)
- Free prs (1 message, latest: Aug 24 2020 at 11:28)
- set_metas with??? (7 messages, latest: Aug 21 2020 at 14:31)
- coqbot comments about allowed-failues (1 message, latest: Aug 20 2020 at 20:35)
- ci-coqhammer failing (2 messages, latest: Aug 19 2020 at 20:12)
- Should coqc send Print to stdout? (2 messages, latest: Aug 19 2020 at 19:55)
- Special care for constraints introduced in OCaml tactic? (9 messages, latest: Aug 18 2020 at 11:47)
- coqide.dev package broken (4 messages, latest: Aug 18 2020 at 07:31)
- Coq CI changes for Iris (1 message, latest: Aug 18 2020 at 06:31)
- coqide.dev broken (2 messages, latest: Aug 18 2020 at 06:28)
- core.identity vs core.eq (1 message, latest: Aug 17 2020 at 16:14)
- Universe levels creation (11 messages, latest: Aug 13 2020 at 22:56)
- Ocaml trace of cbv runs in endless loop (8 messages, latest: Aug 12 2020 at 08:25)
- Old coqdev mailing list archives? (3 messages, latest: Aug 10 2020 at 20:32)
- GitHub mobile apps for Coq development (5 messages, latest: Aug 10 2020 at 15:34)
- motivation for native implementations (2 messages, latest: Aug 10 2020 at 10:03)
- Performance testing (32 messages, latest: Aug 06 2020 at 17:18)
- coqbot merge metadata (2 messages, latest: Aug 05 2020 at 13:58)
- `Case` constructor taking less arguments in 8.12 (2 messages, latest: Aug 04 2020 at 09:08)
- ocamlfind numeral_notation (67 messages, latest: Aug 03 2020 at 16:49)
- Eta reduction (3 messages, latest: Jul 31 2020 at 10:27)
- Overly restrictive universe constraints (3 messages, latest: Jul 30 2020 at 07:37)
- Maintaining a library of formal mathematics (4 messages, latest: Jul 29 2020 at 21:28)
- Coq Platform Discussion (1 message, latest: Jul 29 2020 at 14:07)
- 8.12 coq platform release thread (2 messages, latest: Jul 29 2020 at 14:05)
- Testing the signed installers for 8.12.0 (35 messages, latest: Jul 28 2020 at 17:52)
- coqdoc double counting newlines (4 messages, latest: Jul 25 2020 at 16:35)
- dune and test-suite (46 messages, latest: Jul 24 2020 at 17:20)
- testing coqdoc on sf? (1 message, latest: Jul 24 2020 at 13:20)
- Ignoring "Nothing to inject" warnings (5 messages, latest: Jul 24 2020 at 08:44)
- Notations (6 messages, latest: Jul 23 2020 at 19:14)
- What is going on with CI? (12 messages, latest: Jul 23 2020 at 13:15)
- tryif & anomalies (3 messages, latest: Jul 23 2020 at 09:57)
- Cygwin server for Windows build seems to be down (4 messages, latest: Jul 23 2020 at 09:19)
- Extraction related issues (4 messages, latest: Jul 22 2020 at 19:30)
- set_term_pr (2 messages, latest: Jul 22 2020 at 11:37)
- Pendulum (11 messages, latest: Jul 21 2020 at 14:05)
- admit-like tactic (3 messages, latest: Jul 21 2020 at 10:59)
- OSX package build (27 messages, latest: Jul 18 2020 at 11:43)
- Error message on wrong-compiled .vo files in 8.12 (3 messages, latest: Jul 16 2020 at 17:28)
- Serious Stdlib coqdoc regression in 8.12 with links (9 messages, latest: Jul 16 2020 at 16:58)
- CUDW2020 (26 messages, latest: Jul 16 2020 at 16:36)
- Paper review request (21 messages, latest: Jul 13 2020 at 11:35)
- Design question: propagating scopes beyond `.(@p)` notation? (1 message, latest: Jul 13 2020 at 08:54)
- Porting plugins to dune (4 messages, latest: Jul 11 2020 at 15:06)
- Detecting stuckness in CClosure reduction (12 messages, latest: Jul 10 2020 at 15:34)
- fiat-crypto-ocaml failing (3 messages, latest: Jul 09 2020 at 21:11)
- Per definition typing_flags (6 messages, latest: Jul 06 2020 at 14:32)
- Need help with ocamlfind (36 messages, latest: Jul 06 2020 at 06:57)
- Instantiating Evars (9 messages, latest: Jul 04 2020 at 14:45)
- spurious metacoq failure? (4 messages, latest: Jul 01 2020 at 12:13)
- CI job test-suite:4.12+trunk+dune (1 message, latest: Jun 29 2020 at 15:06)
- rewrite matching algorithms (2 messages, latest: Jun 27 2020 at 21:00)
- related-tools on Coq website (9 messages, latest: Jun 25 2020 at 16:35)
- jenkins date (2 messages, latest: Jun 24 2020 at 15:58)
- Quick question about native (41 messages, latest: Jun 24 2020 at 13:47)
- Potential bug with Params and prim. projections? (9 messages, latest: Jun 23 2020 at 15:35)
- test-suite/bugs/bug_*.v (1 message, latest: Jun 23 2020 at 12:15)
- How to print large terms (7 messages, latest: Jun 22 2020 at 19:30)
- coq-performance-tests (1 message, latest: Jun 22 2020 at 18:25)
- CI DAG view (3 messages, latest: Jun 19 2020 at 15:40)
- Coq 8.11.2 release plans (92 messages, latest: Jun 19 2020 at 14:35)
- eauto unification (14 messages, latest: Jun 19 2020 at 13:37)
- Discrimination trees & typeclass search (62 messages, latest: Jun 19 2020 at 09:33)
- Reference manual (3 messages, latest: Jun 17 2020 at 15:55)
- rewriting (6 messages, latest: Jun 17 2020 at 15:51)
- Pre-call for volunteers to improve the manual (1 message, latest: Jun 16 2020 at 17:59)
- Experiences from Exporting Major Proof Assistant Libraries (19 messages, latest: Jun 16 2020 at 11:15)
- Printing an evar (8 messages, latest: Jun 15 2020 at 22:06)
- lines of code in Coq's CI (12 messages, latest: Jun 15 2020 at 21:46)
- `par:` documentation (8 messages, latest: Jun 15 2020 at 18:00)
- Verifying signatures of Coq release tarballs (62 messages, latest: Jun 15 2020 at 15:23)
- Inria gforge end-of-life and Coq packages (29 messages, latest: Jun 14 2020 at 14:27)
- Opam pin add not working as supposed (7 messages, latest: Jun 13 2020 at 16:28)
- `unshelve` and order of subgoals (28 messages, latest: Jun 13 2020 at 03:34)
- Coercions used when printing themselves (3 messages, latest: Jun 12 2020 at 23:24)
- V8.12+beta1 tag (3 messages, latest: Jun 12 2020 at 22:50)
- Reachable evarmaps (47 messages, latest: Jun 12 2020 at 15:29)
- Fail catches anomaly and errors the same way (4 messages, latest: Jun 12 2020 at 13:25)
- Semantics of assert by (16 messages, latest: Jun 12 2020 at 13:20)
- coqbot services (1 message, latest: Jun 12 2020 at 11:40)
- coqbot rebase tags for coq-opam-archive (1 message, latest: Jun 12 2020 at 11:40)
- Switching to dune (the compilation of Coq) (14 messages, latest: Jun 11 2020 at 13:04)
- OMDoc theory exporting (9 messages, latest: Jun 11 2020 at 09:40)
- V82 compat layer (19 messages, latest: Jun 10 2020 at 20:40)
- declaring arbitrary terms as hints is deprecated (111 messages, latest: Jun 10 2020 at 16:52)
- four-color takes more time on coq-dev (12 messages, latest: Jun 10 2020 at 15:23)
- Printing options (6 messages, latest: Jun 10 2020 at 14:54)
- Excluding constants from Search (10 messages, latest: Jun 10 2020 at 13:36)
- Building Gappa Plugin (1 message, latest: Jun 09 2020 at 20:28)
- min OCaml version for 8.12 (and 8.13) (9 messages, latest: Jun 06 2020 at 04:34)
- CClosure Cache & Universes (35 messages, latest: Jun 05 2020 at 21:37)
- Github Actions (6 messages, latest: Jun 05 2020 at 11:49)
- Windows build issue (28 messages, latest: Jun 04 2020 at 22:25)
- Version constraints for Plugins (15 messages, latest: Jun 04 2020 at 21:35)
- firstorder tactic limitations (3 messages, latest: Jun 04 2020 at 11:36)
- Parsing interface (63 messages, latest: Jun 03 2020 at 12:07)
- Moving Unicoq to Coq (18 messages, latest: Jun 02 2020 at 20:13)
- Pp.t to HTML (7 messages, latest: Jun 02 2020 at 11:50)
- Canonical Structures (97 messages, latest: May 29 2020 at 11:58)
- Resolving PR Feedback (7 messages, latest: May 28 2020 at 12:56)
- Keeping opam packages in sync. (8 messages, latest: May 28 2020 at 10:24)
- Async test-suite failure (22 messages, latest: May 25 2020 at 20:40)
- Universe minimization for Props (1 message, latest: May 22 2020 at 14:02)
- Ltac2 roadmap (9 messages, latest: May 22 2020 at 07:40)
- Github Notifications (3 messages, latest: May 21 2020 at 22:16)
- Github Noisy Notifications (1 message, latest: May 21 2020 at 20:14)
- Github Push Notifications (1 message, latest: May 21 2020 at 20:13)
- Dune Test suite Failure (5 messages, latest: May 20 2020 at 16:19)
- Elpi's CI (2 messages, latest: May 19 2020 at 07:56)
- History (3 messages, latest: May 18 2020 at 11:44)
- Building Sphinx documentation (11 messages, latest: May 15 2020 at 12:53)
- coqdep (1 message, latest: May 13 2020 at 19:03)
- Coq & `perf` (16 messages, latest: May 13 2020 at 10:35)
- Spurious failure with primitive floats and native compile (4 messages, latest: May 13 2020 at 09:17)
- Overlays (3 messages, latest: May 13 2020 at 08:04)
- Display of `.. coqtop::` with coqdoc (4 messages, latest: May 12 2020 at 16:58)
- inconsistent Hurkens (3 messages, latest: May 12 2020 at 00:34)
- Merge script (10 messages, latest: May 11 2020 at 12:54)
- Proof checking performance (5 messages, latest: May 11 2020 at 04:42)
- [release team] 8.12 milestone (3 messages, latest: May 09 2020 at 19:37)
- GitLab 13.0 (2 messages, latest: May 09 2020 at 15:34)
- Coq code formatting (13 messages, latest: May 09 2020 at 15:26)
- Linking issues/PR (1 message, latest: May 07 2020 at 18:57)
- branching of 8.12 and pinning addons (3 messages, latest: May 07 2020 at 08:20)
- imported from gitter room coq/coq (91224 messages, latest: May 06 2020 at 00:48)
- Issue triaging (31 messages, latest: Feb 20 2019 at 14:36)
Last updated: Mar 25 2023 at 07:28 UTC