Stream: Coq devs & plugin devs

Topics:

• [CI] Remove library-undecidability (10 messages, latest: Oct 08 2024 at 13:55)
• Convergence of auto, eauto and typeclasses eauto tactics? (7 messages, latest: Oct 08 2024 at 08:11)
• itree failure in CI (1 message, latest: Oct 07 2024 at 14:32)
• New Discourse topics (64 messages, latest: Oct 05 2024 at 04:19)
• A bug in the implementation of `Add Field`, I believe... (1 message, latest: Oct 04 2024 at 20:20)
• Rocq roadmap (9 messages, latest: Oct 04 2024 at 20:18)
• Where is the ring structure for real numbers declared? (8 messages, latest: Oct 04 2024 at 08:54)
• ci-coq-02 down (2 messages, latest: Oct 03 2024 at 11:41)
• Towards a common done (57 messages, latest: Oct 01 2024 at 12:10)
• ✔ Generate a fresh constant name (8 messages, latest: Oct 01 2024 at 10:22)
• ✔ Threading the environment and evar map (2 messages, latest: Oct 01 2024 at 10:03)
• Threading the environment and evar map (2 messages, latest: Sep 30 2024 at 20:13)
• Understanding QSort and QVar (7 messages, latest: Sep 30 2024 at 14:05)
• Global environment in plugin Command (11 messages, latest: Sep 26 2024 at 13:11)
• elpi broken in CI (1 message, latest: Sep 25 2024 at 12:34)
• ✔ Global environment in plugin Command (5 messages, latest: Sep 24 2024 at 10:52)
• UnivSubst.nf_evars_and_universes_opt_subst deprecation (9 messages, latest: Sep 23 2024 at 15:12)
• OCAMLPATH in local ci (6 messages, latest: Sep 20 2024 at 22:23)
• CI runners (84 messages, latest: Sep 19 2024 at 16:51)
• Coq-Elpi CI (2 messages, latest: Sep 19 2024 at 14:48)
• looking for assignee (41 messages, latest: Sep 19 2024 at 09:21)
• Renamig tasks (40 messages, latest: Sep 18 2024 at 14:34)
• Pattern-matching and mutable in OCaml (6 messages, latest: Sep 18 2024 at 10:39)
• Type inverence on komplex match statement (1 message, latest: Sep 18 2024 at 08:42)
• Relevance of projections (9 messages, latest: Sep 17 2024 at 10:03)
• Adding Sorts (36 messages, latest: Sep 17 2024 at 09:39)
• Adding rewrite rules for existing constants (8 messages, latest: Sep 15 2024 at 23:45)
• Possible levels for qualities other than SProp, Prop, Set. (17 messages, latest: Sep 14 2024 at 14:41)
• How to add hints to hint databases by using Coq API (1 message, latest: Sep 13 2024 at 16:26)
• 8.20.1 (8 messages, latest: Sep 13 2024 at 14:09)
• opam pin does not work with a git url (12 messages, latest: Sep 11 2024 at 18:26)
• 8.20 (40 messages, latest: Sep 11 2024 at 15:08)
• coqeal universe issues (4 messages, latest: Sep 11 2024 at 12:10)
• Rewrite rule syntax (7 messages, latest: Sep 11 2024 at 09:48)
• coq quiz (16 messages, latest: Sep 11 2024 at 08:20)
• examples in bedrock2 take a long time (4 messages, latest: Sep 10 2024 at 18:46)
• Access lemma database from plugin (10 messages, latest: Sep 10 2024 at 06:58)
• Future-proof Require from Stdlib (35 messages, latest: Sep 09 2024 at 15:45)
• firstn/skipn vs take/drop (10 messages, latest: Sep 02 2024 at 21:53)
• coq call (731 messages, latest: Sep 02 2024 at 12:45)
• Some strange about glob of references (3 messages, latest: Aug 30 2024 at 09:13)
• Strange results from coqdep on Windows / Meta file question (48 messages, latest: Aug 23 2024 at 16:42)
• Custom docker images automation for CIs (78 messages, latest: Aug 20 2024 at 18:57)
• ✔ Get inductive type definition when implementing a tactic (11 messages, latest: Aug 08 2024 at 15:50)
• Cannot extract nontrivial sort polymorphism (20 messages, latest: Aug 05 2024 at 13:47)
• Equality of local bound variables? (5 messages, latest: Aug 05 2024 at 08:41)
• ✔ eexists without intro causes scoping errors (6 messages, latest: Aug 02 2024 at 07:51)
• Presence or availability for the 2024 Coq Workshop (1 message, latest: Aug 01 2024 at 14:58)
• PR looking for assignee (1 message, latest: Jul 30 2024 at 11:20)
• Conditional coercions? (21 messages, latest: Jul 29 2024 at 09:19)
• non-reference term in "using" clauses is deprecated (15 messages, latest: Jul 29 2024 at 08:36)
• AlphaProof & AlphaGeometry2 at maths olympiad (2 messages, latest: Jul 26 2024 at 11:31)
• /usr/doc/coqide/FAQ (2 messages, latest: Jul 26 2024 at 06:38)
• CClosure and σ-calculus (13 messages, latest: Jul 24 2024 at 18:21)
• ✔ Changes in setoid_rewrite between 8.17 and 8.18? (2 messages, latest: Jul 23 2024 at 17:40)
• Head reduction of `match` with Definitional UIP? (5 messages, latest: Jul 23 2024 at 16:32)
• Changes in setoid_rewrite between 8.17 and 8.18? (1 message, latest: Jul 23 2024 at 16:19)
• elpi ocaml-lsp-server (5 messages, latest: Jul 23 2024 at 14:06)
• Implementation of Rewrite Tactic for setoid equivalences (4 messages, latest: Jul 22 2024 at 17:29)
• opam version in bench (4 messages, latest: Jul 22 2024 at 14:03)
• shift vs lift for explicit substitutions (1 message, latest: Jul 16 2024 at 14:56)
• ✔ Bench broken (missing pkg-config) (11 messages, latest: Jul 15 2024 at 15:51)
• Findlib warnings in OCaml 5 (4 messages, latest: Jul 15 2024 at 14:09)
• ✔ Ltac2 FFI : building types and constructors (5 messages, latest: Jul 11 2024 at 16:58)
• Ltac2 FFI : building types and constructors (2 messages, latest: Jul 11 2024 at 14:01)
• ✔ Calling Ltac2 from Ocaml (11 messages, latest: Jul 11 2024 at 13:38)
• Create a fresh evar using Ltac2 (1 message, latest: Jul 11 2024 at 11:47)
• evarconv and primproj (29 messages, latest: Jul 11 2024 at 11:31)
• Removing _build/blabla from file names in error messages (5 messages, latest: Jul 10 2024 at 11:52)
• Calling Ltac2 from Ocaml (7 messages, latest: Jul 10 2024 at 10:38)
• Equations tag for 8.20 (2 messages, latest: Jul 09 2024 at 10:39)
• Programmatically define pattern matching (7 messages, latest: Jul 08 2024 at 10:55)
• Not able to compile plugin tutorial tuto1 (8 messages, latest: Jul 08 2024 at 09:34)
• gitlab.inria.fr storage quotas (7 messages, latest: Jul 05 2024 at 14:40)
• speeding up windows CI (6 messages, latest: Jul 04 2024 at 15:48)
• ✔ Documentation for using proof-general to edit standard lib (2 messages, latest: Jul 04 2024 at 11:47)
• Documentation for using proof-general to edit standard lib (2 messages, latest: Jul 04 2024 at 05:24)
• ✔ 8.20+rc1 and VSCoq (3 messages, latest: Jul 03 2024 at 16:08)
• Explanation of Impargs.implicit_position (2 messages, latest: Jul 01 2024 at 15:15)
• cudw 2024 (2 messages, latest: Jul 01 2024 at 12:56)
• 8.19.2 (48 messages, latest: Jun 29 2024 at 13:57)
• CI breakage (19 messages, latest: Jun 21 2024 at 21:12)
• Deactivating Arguments' "simpl" flags? (2 messages, latest: Jun 20 2024 at 18:35)
• master merging rules (5 messages, latest: Jun 20 2024 at 12:23)
• Cannot compile Coq (caml_mutex_unlock not available) (3 messages, latest: Jun 19 2024 at 16:29)
• Ctrl-Z in make ci-foo (4 messages, latest: Jun 17 2024 at 19:18)
• Docker-Coq CI rebuilds (3 messages, latest: Jun 14 2024 at 10:35)
• ✔ Evar contexts & Evd.restrict/Evarutil.restrict_evar (2 messages, latest: Jun 13 2024 at 15:45)
• Evar contexts & Evd.restrict/Evarutil.restrict_evar (1 message, latest: Jun 13 2024 at 13:33)
• pkg:nix ci failure (1 message, latest: Jun 13 2024 at 10:06)
• Equality of constr under different context (12 messages, latest: Jun 12 2024 at 18:41)
• Way to disable universe annotations (7 messages, latest: Jun 10 2024 at 12:33)
• Coq Call, June 4 20204 notes (15 messages, latest: Jun 10 2024 at 08:15)
• Small uniformity of naming and structure in entries.ml? (51 messages, latest: Jun 09 2024 at 14:44)
• ✔ What's up with coq_lsp in CI? (6 messages, latest: Jun 08 2024 at 14:40)
• Allowing several names for the same argument? (1 message, latest: Jun 08 2024 at 11:17)
• Treatment of abstract in the declare.ml execution paths (7 messages, latest: Jun 08 2024 at 10:48)
• requesting quick revert (16 messages, latest: Jun 07 2024 at 16:24)
• ci-serapi failure (8 messages, latest: Jun 07 2024 at 16:03)
• Backport management (3 messages, latest: Jun 03 2024 at 15:23)
• inria gitlab maintenance (2 messages, latest: Jun 03 2024 at 08:07)
• In need of a review for a tutorial about Require and Import (1 message, latest: Jun 01 2024 at 17:05)
• Named hint externs (12 messages, latest: May 31 2024 at 12:05)
• ✔ Coq.Init.Datatypes.nat does not appear in env (1 message, latest: May 30 2024 at 21:32)
• Future computations (93 messages, latest: May 30 2024 at 11:51)
• Libpath of Constant.t (3 messages, latest: May 30 2024 at 10:06)
• Memtrace observations (58 messages, latest: May 29 2024 at 13:54)
• What to think about mono constraints in poly constants? (15 messages, latest: May 28 2024 at 10:45)
• Coq.Init.Datatypes.nat does not appear in env (5 messages, latest: May 27 2024 at 20:41)
• Using sealed for opaque in the code (1 message, latest: May 22 2024 at 06:04)
• Scheme Equality uses opaque andb_prop (6 messages, latest: May 21 2024 at 18:16)
• Issue with Inductive.instantiate_context (5 messages, latest: May 21 2024 at 17:53)
• template poly redesign (1 message, latest: May 21 2024 at 12:44)
• ci-autosubst_ocaml (2 messages, latest: May 20 2024 at 12:07)
• Treatment of universes in the declare.ml execution paths (27 messages, latest: May 20 2024 at 10:02)
• ✔ Explanation of kernel/esubst.ml (90 messages, latest: May 18 2024 at 12:20)
• Explanation of kernel/esubst.ml (1 message, latest: May 17 2024 at 22:21)
• A sealed/unsealed attribute (6 messages, latest: May 17 2024 at 16:17)
• XML protocol failure location (1 message, latest: May 17 2024 at 10:02)
• ✔ Finding the implicit arguments of a constant (2 messages, latest: May 16 2024 at 16:25)
• Finding the implicit arguments of a constant (2 messages, latest: May 16 2024 at 14:14)
• Coq Platform docs (1 message, latest: May 15 2024 at 15:45)
• status of eexact (9 messages, latest: May 15 2024 at 13:50)
• block abstract (9 messages, latest: May 14 2024 at 15:06)
• Merging execution paths for [Program] Fixpoint ... [:= ... (17 messages, latest: May 14 2024 at 15:03)
• String.map function (3 messages, latest: May 14 2024 at 14:08)
• Ltac2 tactic plugins (5 messages, latest: May 14 2024 at 13:19)
• combined coq binaries (11 messages, latest: May 14 2024 at 12:55)
• ✔ Change platform-docs to web public (2 messages, latest: May 14 2024 at 11:52)
• Change platform-docs to web public (1 message, latest: May 14 2024 at 00:06)
• Date poll for discussion on `declare.ml` (20 messages, latest: May 13 2024 at 07:19)
• Bench for stdlib (11 messages, latest: May 12 2024 at 12:29)
• Coq-Elpi looks broken in the CI (4 messages, latest: May 09 2024 at 15:58)
• [ERROR] The comp** of coq-core.dev failed at "dune subst". (81 messages, latest: May 09 2024 at 11:47)
• coqc hangs on QED with latest MacOS/Xcode - works fine with (14 messages, latest: May 08 2024 at 17:34)
• no dunestrap? (10 messages, latest: May 02 2024 at 13:45)
• issue classes (2 messages, latest: May 02 2024 at 12:59)
• ✔ UIP in SProp changes in Coq 8.13 (1 message, latest: May 01 2024 at 23:50)
• UIP in SProp changes in Coq 8.13 (17 messages, latest: May 01 2024 at 20:54)
• ✔ Primitive projections able to eta reduce terms it shoul... (24 messages, latest: May 01 2024 at 15:47)
• Primitive projections able to eta reduce terms it shouldn't (3 messages, latest: May 01 2024 at 14:56)
• ✔ Tag of Mtac2 for 8.19 (6 messages, latest: Apr 26 2024 at 13:15)
• coqbot message (4 messages, latest: Apr 24 2024 at 12:28)
• Is master broken? (5 messages, latest: Apr 24 2024 at 11:34)
• Tag of Mtac2 (3 messages, latest: Apr 24 2024 at 09:01)
• Coq on opam on Mac on OCaml 4.11.1 on GitHub Actions? (2 messages, latest: Apr 23 2024 at 22:41)
• Declare.declare_definition in Coq 8.12 (22 messages, latest: Apr 23 2024 at 20:57)
• Hint opacity, primitive projections, and sections (6 messages, latest: Apr 22 2024 at 15:49)
• Status of fix_undefined_universes? (3 messages, latest: Apr 19 2024 at 17:16)
• ✔ Best way to fix #18920 (evars leak in obligation mode) (1 message, latest: Apr 19 2024 at 16:49)
• Best way to fix #18920 (evars leak in obligation mode) (3 messages, latest: Apr 19 2024 at 15:27)
• Updating Coq to 8.19 in Debian (46 messages, latest: Apr 18 2024 at 13:48)
• closing old PRs (1 message, latest: Apr 17 2024 at 13:20)
• coqc segfaults on M2 (works fine with M1) (5 messages, latest: Apr 16 2024 at 21:49)
• Program CoFixpoint (9 messages, latest: Apr 16 2024 at 13:29)
• master broken (8 messages, latest: Apr 15 2024 at 15:16)
• ✔ Attendants at yesterday's coq call (1 message, latest: Apr 15 2024 at 08:08)
• ✔ Trying to migrate to Coq 8.18.0 -- anomaly error (2 messages, latest: Apr 15 2024 at 01:33)
• Trying to migrate to Coq 8.18.0 -- anomaly error (8 messages, latest: Apr 12 2024 at 22:42)
• Synterp/Interp and `Lib.current_mp` (43 messages, latest: Apr 12 2024 at 11:48)
• Algebraic universes + new constraint solving integration (10 messages, latest: Apr 11 2024 at 10:46)
• Attendants at yesterday's coq call (4 messages, latest: Apr 10 2024 at 07:20)
• Creating an EConstr variable (2 messages, latest: Apr 09 2024 at 16:03)
• ✔ Issue with universes in VM (2 messages, latest: Apr 09 2024 at 09:29)
• Issue with universes in VM (41 messages, latest: Apr 08 2024 at 16:35)
• duplicated parser state handling? (9 messages, latest: Apr 07 2024 at 19:48)
• Start module with declaremods (9 messages, latest: Apr 07 2024 at 11:05)
• ✔ Universes in instances (1 message, latest: Apr 05 2024 at 16:06)
• Universes in instances (4 messages, latest: Apr 04 2024 at 21:32)
• Unifying the effect of "Program" (10 messages, latest: Apr 04 2024 at 13:00)
• Tracing tactics (4 messages, latest: Apr 04 2024 at 07:56)
• ✔ Troubleshooting Dynlink failure (2 messages, latest: Apr 03 2024 at 20:14)
• Troubleshooting Dynlink failure (10 messages, latest: Apr 03 2024 at 19:48)
• test suite live report (1 message, latest: Apr 03 2024 at 15:24)
• theories/omega (1 message, latest: Apr 03 2024 at 13:20)
• Coqlib from the ML side - little example (3 messages, latest: Apr 01 2024 at 10:53)
• 17393 "Allow require to load libraries from memory" (9 messages, latest: Mar 29 2024 at 16:35)
• simple_io broken (1 message, latest: Mar 29 2024 at 12:07)
• Coqlib and deprecated api used in plugin_tutorial (19 messages, latest: Mar 29 2024 at 09:35)
• When does `destruct H` not clear `H`? (7 messages, latest: Mar 28 2024 at 18:27)
• Possible factorization of vtopenproof and vtdefault?? (24 messages, latest: Mar 28 2024 at 08:28)
• Collecting standard term construction (such as "telescope") (2 messages, latest: Mar 26 2024 at 17:24)
• Opam archive cache (5 messages, latest: Mar 26 2024 at 15:02)
• New Goptions API (2 messages, latest: Mar 26 2024 at 11:11)
• New feature that is currently unusable (4 messages, latest: Mar 25 2024 at 17:42)
• Printing Constr.constr with more info (4 messages, latest: Mar 25 2024 at 11:34)
• Coq & frame pointers (3 messages, latest: Mar 25 2024 at 06:53)
• transitive needs: in .gitlab-ci.yml (2 messages, latest: Mar 21 2024 at 20:09)
• Checking individual theorems. (56 messages, latest: Mar 21 2024 at 11:51)
• make world and dune profiles (1 message, latest: Mar 20 2024 at 15:32)
• Post-Coq Call Stdlib CEP discussion (17 messages, latest: Mar 20 2024 at 08:38)
• Anomaly: Already used warning name profile-invalid-stack-no- (4 messages, latest: Mar 19 2024 at 12:49)
• ✔ Making plugin by modifying official template (6 messages, latest: Mar 16 2024 at 12:09)
• Using the Coq core library (7 messages, latest: Mar 15 2024 at 07:29)
• Debugging hangs (5 messages, latest: Mar 14 2024 at 18:19)
• cudw 2024? (7 messages, latest: Mar 13 2024 at 10:30)
• Coq 8.19.1 in Debian (4 messages, latest: Mar 13 2024 at 09:57)
• Setting reduction flags for custom normalization (5 messages, latest: Mar 12 2024 at 23:05)
• deprecate Coq.Sets? (44 messages, latest: Mar 12 2024 at 15:56)
• issue templates (8 messages, latest: Mar 12 2024 at 14:43)
• Modify order of parameters in mul_sub_distr_l (6 messages, latest: Mar 10 2024 at 16:05)
• coq-bench for opam (1872 messages, latest: Mar 10 2024 at 11:16)
• pending change: Docker-Coq default umask: feel free to react (1 message, latest: Mar 06 2024 at 21:50)
• When does `new_type_evar` return an instantiated evar? (21 messages, latest: Mar 05 2024 at 22:29)
• Elpi's coq-master with elpi 1.18.2 (2 messages, latest: Mar 05 2024 at 14:36)
• 8.19 (168 messages, latest: Mar 05 2024 at 00:13)
• 8.19.1 (6 messages, latest: Mar 04 2024 at 13:09)
• Delimiting keyword for definitions defined by tactics (18 messages, latest: Mar 04 2024 at 12:48)
• Review PR about nth_error lemmas in stdlib? (5 messages, latest: Mar 04 2024 at 11:51)
• More prominent documentation of Ltac2? (21 messages, latest: Mar 02 2024 at 12:17)
• ✔ Giving opam access to a specific commit on coq (1 message, latest: Feb 29 2024 at 14:07)
• Giving opam access to a specific commit on coq (7 messages, latest: Feb 29 2024 at 09:53)
• How do we fix #18281? (115 messages, latest: Feb 28 2024 at 09:45)
• Catching timeout from withing the proofview monad (17 messages, latest: Feb 27 2024 at 15:31)
• ✔ Need a little help with fixing AAC tactics (1 message, latest: Feb 26 2024 at 18:52)
• Need a little help with fixing AAC tactics (36 messages, latest: Feb 26 2024 at 13:43)
• Design of primitive projections (3 messages, latest: Feb 26 2024 at 08:04)
• custom runner (10 messages, latest: Feb 23 2024 at 14:01)
• Changes in coq opam archive not picked up by opam? (13 messages, latest: Feb 23 2024 at 09:18)
• ✔ Changes in coq opam archive not picked up by opam? (3 messages, latest: Feb 22 2024 at 14:09)
• Does lia/uint63 need care to prevent blowup? (8 messages, latest: Feb 22 2024 at 10:34)
• Evar normalization during case pretyping (6 messages, latest: Feb 21 2024 at 13:35)
• Notation printing change in 8.19 branch (13 messages, latest: Feb 20 2024 at 16:08)
• CI docker images? (26 messages, latest: Feb 20 2024 at 12:03)
• How to fix Windows CI in PR (2 messages, latest: Feb 15 2024 at 21:05)
• TC and eta for functions (7 messages, latest: Feb 14 2024 at 10:47)
• ✔ SKIP src/ornaments.cmxs since it has no logical path (2 messages, latest: Feb 14 2024 at 00:41)
• SKIP src/ornaments.cmxs since it has no logical path (2 messages, latest: Feb 13 2024 at 20:59)
• ✔ Findlib warning (1 message, latest: Feb 13 2024 at 20:09)
• ✔ Update on BigNums (2 messages, latest: Feb 13 2024 at 17:33)
• Update on BigNums (5 messages, latest: Feb 13 2024 at 16:34)
• Entirely useless inlining annotations (13 messages, latest: Feb 12 2024 at 15:55)
• Status of native_compute on MacOS (28 messages, latest: Feb 11 2024 at 01:35)
• Meaning of subst and discharge in Libobject (12 messages, latest: Feb 10 2024 at 20:44)
• What happens when a module ends? (6 messages, latest: Feb 10 2024 at 16:41)
• Managing tables for persistent data (4 messages, latest: Feb 10 2024 at 10:04)
• iris broken in CI (1 message, latest: Feb 09 2024 at 16:49)
• cbv +[constants] (7 messages, latest: Feb 09 2024 at 15:03)
• Sizes reported by votour (23 messages, latest: Feb 08 2024 at 12:46)
• Findlib warning (3 messages, latest: Feb 08 2024 at 06:23)
• Adding Loadpath using -R in _CoqProject (33 messages, latest: Feb 07 2024 at 19:52)
• Expanding the constant used for partially-applied prim.proj. (1 message, latest: Feb 07 2024 at 08:26)
• CoqIDE Failing in Coq Platform CI on Windows since 2 days (2 messages, latest: Feb 05 2024 at 15:06)
• state of `make test-suite` and `test-suite/dune` (1 message, latest: Feb 03 2024 at 12:13)
• Sharing in vm bytecode (5 messages, latest: Feb 03 2024 at 12:09)
• RC advertising (4 messages, latest: Feb 02 2024 at 14:16)
• RC advertizing (6 messages, latest: Feb 02 2024 at 10:56)
• runners (51 messages, latest: Feb 02 2024 at 09:21)
• Debugging printer for RedFlag.reds (5 messages, latest: Feb 01 2024 at 18:06)
• assignee for CI fix (2 messages, latest: Feb 01 2024 at 17:46)
• match with alias (22 messages, latest: Jan 31 2024 at 12:33)
• Systematically refolding named fix/cofix (1 message, latest: Jan 31 2024 at 09:41)
• coqbot documentation (2 messages, latest: Jan 30 2024 at 09:52)
• call day (2 messages, latest: Jan 29 2024 at 19:53)
• inconsist. assump. over stdlib with opam installing coq 8.18 (12 messages, latest: Jan 29 2024 at 14:16)
• ci-coq_library_undecidability broken in CI (metacoq update) (2 messages, latest: Jan 29 2024 at 13:30)
• metacoq broken in CI (3 messages, latest: Jan 27 2024 at 19:06)
• How to pass coq flags to sphinx (9 messages, latest: Jan 26 2024 at 21:48)
• coq-http broken in CI (1 message, latest: Jan 26 2024 at 20:17)
• Variant -V option for Coq Library Loadpaths (138 messages, latest: Jan 25 2024 at 15:55)
• Loadpath algorithm (17 messages, latest: Jan 25 2024 at 11:44)
• ✔ Analysis broken in CI (1 message, latest: Jan 24 2024 at 18:28)
• Remove Include Type (13 messages, latest: Jan 24 2024 at 18:23)
• Analysis broken in CI (1 message, latest: Jan 24 2024 at 15:04)
• ✔ coq.dev opam package broken? (23 messages, latest: Jan 24 2024 at 14:32)
• ✔ Passing filters in open_function in libobject.mli (2 messages, latest: Jan 23 2024 at 22:45)
• Passing filters in open_function in libobject.mli (2 messages, latest: Jan 23 2024 at 20:30)
• Zeuclid and ZDivEucl (2 messages, latest: Jan 23 2024 at 18:27)
• Status of Coq.Numbers.NatInt.NZDomain.v in the stdlib (5 messages, latest: Jan 23 2024 at 15:32)
• What is the `Arith.Bool_nat` file for? (5 messages, latest: Jan 23 2024 at 15:13)
• unimath broken on master (4 messages, latest: Jan 23 2024 at 09:54)
• Primitive arrays max length (14 messages, latest: Jan 21 2024 at 14:58)
• coqpl dev session (1 message, latest: Jan 20 2024 at 11:58)
• ✔ gitlabpages.inria.fr unstable since yesterday (2 messages, latest: Jan 19 2024 at 13:13)
• status of 8.18.1 (2 messages, latest: Jan 18 2024 at 15:10)
• gitlabpages.inria.fr unstable since yesterday (4 messages, latest: Jan 18 2024 at 10:45)
• new inconsistency (1 message, latest: Jan 16 2024 at 13:41)
• credits for 8.19 (19 messages, latest: Jan 15 2024 at 16:17)
• Ltac2 in theories or theories/Init (23 messages, latest: Jan 15 2024 at 10:05)
• Names used in extraction plugins (12 messages, latest: Jan 12 2024 at 12:49)
• Test-suite broken on unit tests (16 messages, latest: Jan 12 2024 at 10:44)
• Goptions vs grammar file (3 messages, latest: Jan 12 2024 at 08:43)
• Check if name is constant or function? (10 messages, latest: Jan 11 2024 at 18:55)
• Having a string template (5 messages, latest: Jan 11 2024 at 18:17)
• Cannot deprecate a Module Type (3 messages, latest: Jan 10 2024 at 18:06)
• ✔ Add LoadPath vs Add Rec Loadpath (3 messages, latest: Jan 09 2024 at 20:44)
• Unable to reduce under opaque constant during unification (7 messages, latest: Jan 09 2024 at 19:13)
• canonical structure vs. simplification (3 messages, latest: Jan 09 2024 at 14:40)
• github having issues (2 messages, latest: Jan 09 2024 at 14:20)
• Making plugin by modifying official template (5 messages, latest: Jan 09 2024 at 09:47)
• bug minimizer broken (1 message, latest: Jan 09 2024 at 09:21)
• Numbers Arith, ZArith, etc and missing lemmas (7 messages, latest: Jan 09 2024 at 08:07)
• Proving lemmas about N and positive using Z (7 messages, latest: Jan 08 2024 at 12:27)
• ✔ coqdoc named anchors in generated HTML (3 messages, latest: Jan 07 2024 at 16:59)
• coqdoc named anchors in generated HTML (3 messages, latest: Jan 07 2024 at 11:36)
• Bench for mathcomp broken (5 messages, latest: Jan 04 2024 at 16:46)
• PR Review (4 messages, latest: Jan 03 2024 at 21:11)
• remove deprecated files in Arith? (53 messages, latest: Jan 03 2024 at 12:49)
• Add LoadPath vs Add Rec Loadpath (4 messages, latest: Jan 02 2024 at 20:29)
• Spack package manager (1 message, latest: Jan 02 2024 at 10:35)
• How to organize a collection of notes/issues (3 messages, latest: Jan 01 2024 at 20:20)
• ✔ Docker-sponsored OSS membership renewal submitted for c... (2 messages, latest: Jan 01 2024 at 11:17)
• Display of implicit arguments in Print vs About (12 messages, latest: Dec 30 2023 at 18:21)
• Docker-sponsored OSS membership renewal submitted for coqorg (2 messages, latest: Dec 29 2023 at 22:38)
• uid in docker images (1 message, latest: Dec 25 2023 at 23:41)
• ✔ About "private" in Coq (9 messages, latest: Dec 25 2023 at 18:27)
• About "private" in Coq (Was: Init is too big) (41 messages, latest: Dec 23 2023 at 22:44)
• bench 8.19 vs 8.18 (3 messages, latest: Dec 22 2023 at 13:11)
• Retroknowledge? (18 messages, latest: Dec 21 2023 at 09:27)
• Init is too big (24 messages, latest: Dec 21 2023 at 08:49)
• Coq Working Group December 2023 (21 messages, latest: Dec 20 2023 at 14:42)
• When to share universes when declaring multiple variables? (7 messages, latest: Dec 17 2023 at 10:14)
• CI machines (2 messages, latest: Dec 17 2023 at 09:41)
• Where does the initial loadpath come from? (4 messages, latest: Dec 16 2023 at 13:36)
• Problems with CI and overlays (3 messages, latest: Dec 15 2023 at 12:43)
• Enough privileges to tweak issues/PR tags (13 messages, latest: Dec 15 2023 at 10:16)
• Bug?: position of reference of notations in glob file (4 messages, latest: Dec 15 2023 at 09:12)
• Menhir (20 messages, latest: Dec 14 2023 at 11:40)
• How to deprecate files in the stdlib? (24 messages, latest: Dec 13 2023 at 18:38)
• gitlab.mpi-sws.org down (2 messages, latest: Dec 13 2023 at 16:08)
• TC search and modulo_eta (5 messages, latest: Dec 13 2023 at 11:04)
• Validation bug? (7 messages, latest: Dec 12 2023 at 20:31)
• CI Errors (23 messages, latest: Dec 12 2023 at 06:20)
• requesting assignee to fix master (1 message, latest: Dec 11 2023 at 11:05)
• Merge of the code paths for Variables and Context (1 message, latest: Dec 10 2023 at 16:50)
• Semantic of injection/discriminate with? (1 message, latest: Dec 09 2023 at 11:44)
• GitHub behaving weirdly (2 messages, latest: Dec 08 2023 at 15:34)
• process for version bump (17 messages, latest: Dec 04 2023 at 14:59)
• Change in behavior of Recordops.lookup_projections (13 messages, latest: Dec 01 2023 at 04:29)
• Use new Coq/coq#18193 in stdlib (3 messages, latest: Nov 29 2023 at 15:32)
• Improving the test-suite? (13 messages, latest: Nov 28 2023 at 10:06)
• ✔ Inria GitLab down (6 messages, latest: Nov 28 2023 at 09:54)
• Track multiple compilations in the CI (40 messages, latest: Nov 28 2023 at 09:31)
• branch delayed (1 message, latest: Nov 27 2023 at 09:23)
• Inria GitLab down (16 messages, latest: Nov 26 2023 at 18:20)
• Coq Calls discussion topic (17 messages, latest: Nov 24 2023 at 17:14)
• nsatz sefgault (66 messages, latest: Nov 22 2023 at 16:20)
• mathcomp word failing (5 messages, latest: Nov 22 2023 at 07:38)
• iris, stdpp, lambdarust and perennial (118 messages, latest: Nov 21 2023 at 16:59)
• Unification issue when a projection is applied (6 messages, latest: Nov 21 2023 at 15:53)
• Coqc colours in the CI? (4 messages, latest: Nov 20 2023 at 10:16)
• make ci-vst (11 messages, latest: Nov 19 2023 at 10:38)
• Target branch for the CI and base branch for a PR (2 messages, latest: Nov 17 2023 at 13:41)
• fiat-crypto slowness (45 messages, latest: Nov 17 2023 at 13:28)
• Hints.add_transparency rebuilding database(s) a lot (32 messages, latest: Nov 13 2023 at 19:52)
• XDG_DATA_DIRS / XDG_DATA_HOME (7 messages, latest: Nov 10 2023 at 17:04)
• building refman: maximum recursion depth exceeded (7 messages, latest: Nov 10 2023 at 16:43)
• ✔ Assertion failed in coq_elpi_HOAS.ml (7 messages, latest: Nov 10 2023 at 13:48)
• NonStuckFailure (6 messages, latest: Nov 09 2023 at 11:45)
• 8.18 missing from opam? (7 messages, latest: Nov 09 2023 at 10:01)
• ✔ Coq Call: does rendevouz work with Safari (3 messages, latest: Nov 09 2023 at 08:26)
• Coq Call: does rendevouz work with Safari (8 messages, latest: Nov 08 2023 at 20:33)
• Possible accidental PR review (1 message, latest: Nov 08 2023 at 14:29)
• Unicode offset in error messages (12 messages, latest: Nov 08 2023 at 11:00)
• CI broken? (10 messages, latest: Nov 08 2023 at 09:23)
• test suite failing in macos (12 messages, latest: Nov 06 2023 at 20:36)
• Focus and Unfocus commands (15 messages, latest: Nov 06 2023 at 11:41)
• fiat-crypto-legacy (3 messages, latest: Nov 05 2023 at 14:22)
• Adding an "information" attribute beside "deprecation" (16 messages, latest: Nov 03 2023 at 13:33)
• Solution for QED "slow" resulting from simpl in hypothesis (5 messages, latest: Nov 03 2023 at 08:37)
• PR reviews for 8.19 (2 messages, latest: Nov 02 2023 at 10:01)
• A shell function to help switching Coq environment (28 messages, latest: Nov 01 2023 at 18:32)
• 8.18.1? (6 messages, latest: Nov 01 2023 at 04:32)
• Attaching metadata to declarations (43 messages, latest: Oct 31 2023 at 07:41)
• ✔ Installation issue (Unbound module Vernactypes) (6 messages, latest: Oct 30 2023 at 15:29)
• Installation issue (Unbound module Vernactypes) (12 messages, latest: Oct 30 2023 at 13:48)
• Universe normalization in `make_local_hint_db` (7 messages, latest: Oct 30 2023 at 13:07)
• coq-bignums for coq 8.14 (7 messages, latest: Oct 28 2023 at 12:16)
• Notations for primitive int63 (3 messages, latest: Oct 28 2023 at 09:43)
• CI dead? (1 message, latest: Oct 26 2023 at 18:07)
• Overlap of recursive presentations of mutual inductive types (3 messages, latest: Oct 25 2023 at 12:36)
• Merging overlay (4 messages, latest: Oct 25 2023 at 10:35)
• Meeting in dec/jan (2 messages, latest: Oct 25 2023 at 10:28)
• Canonical structure instanciation in elpi (2 messages, latest: Oct 25 2023 at 09:12)
• coq-dpdgraph, autoconf, docker-ci (8 messages, latest: Oct 23 2023 at 12:43)
• Using modules as namespaces (46 messages, latest: Oct 22 2023 at 12:41)
• (Modules as namespaces) Shadowing between module aliases (2 messages, latest: Oct 22 2023 at 11:21)
• Experiment with "docstrings" (1 message, latest: Oct 22 2023 at 11:16)
• Distributed builds for Coq (16 messages, latest: Oct 21 2023 at 13:37)
• Coq hangs on Qed (20 messages, latest: Oct 20 2023 at 09:14)
• Unable to build Coq 8.16 with newer Dune (6 messages, latest: Oct 19 2023 at 10:48)
• Lean FRO meeting (97 messages, latest: Oct 19 2023 at 08:05)
• repeat apply an unexisting lemma (13 messages, latest: Oct 18 2023 at 19:00)
• parsing separation API (12 messages, latest: Oct 18 2023 at 14:46)
• Removal of bbv in Coq's CI? (8 messages, latest: Oct 18 2023 at 14:34)
• Reals, (/ 0) and teaching (15 messages, latest: Oct 18 2023 at 06:29)
• auto with zarith calls lia (1 message, latest: Oct 17 2023 at 10:01)
• New dylink error with file without implementation (7 messages, latest: Oct 16 2023 at 14:45)
• Coq 8.18 and MathComp 2 in Debian (14 messages, latest: Oct 13 2023 at 12:43)
• Other candidates for deprecation in the stdlib (2 messages, latest: Oct 12 2023 at 16:45)
• Bench hardware (22 messages, latest: Oct 11 2023 at 13:50)
• Coq website migration (53 messages, latest: Oct 11 2023 at 10:57)
• Test case failing with coqc but succeeds in vscoq/coqide (43 messages, latest: Oct 11 2023 at 10:37)
• Lost with tclFail/tclZERO/raise (11 messages, latest: Oct 10 2023 at 15:56)
• Windows CI is very slow (9 messages, latest: Oct 09 2023 at 14:05)
• ✔ test-suite and ounit2 (2 messages, latest: Oct 07 2023 at 08:42)
• CI minutes and environmental impact (50 messages, latest: Oct 06 2023 at 16:39)
• ✔ Manually installing .v files (1 message, latest: Oct 06 2023 at 14:16)
• Manually installing .v files (18 messages, latest: Oct 06 2023 at 13:58)
• Performance issues in #17839 (6 messages, latest: Oct 06 2023 at 12:17)
• Caching `CClosure.to_constr` calls (2 messages, latest: Oct 06 2023 at 09:07)
• type cast parsing (12 messages, latest: Oct 04 2023 at 20:12)
• ✔ "Anomaly "conversion was given unreduced term (FLambda)... (2 messages, latest: Oct 04 2023 at 14:33)
• "Anomaly "conversion was given unreduced term (FLambda)." wi (4 messages, latest: Oct 04 2023 at 06:36)
• ✔ coq calls (1 message, latest: Oct 03 2023 at 14:57)
• Minimal working examples of Coq code (4 messages, latest: Oct 03 2023 at 14:11)
• Migration to Inria GitLab for CI (instead of GitLab.com) (81 messages, latest: Oct 03 2023 at 10:10)
• MathComp failure in CI (4 messages, latest: Oct 03 2023 at 08:21)
• Logic library (23 messages, latest: Oct 01 2023 at 15:13)
• Logics/StrictProp.v (2 messages, latest: Sep 30 2023 at 06:17)
• testing metacoq -quick on CI? (1 message, latest: Sep 30 2023 at 04:30)
• 8.19 plan (45 messages, latest: Sep 29 2023 at 10:03)
• ✔ Printing a GlobRef.Map as (key, value) pairs (4 messages, latest: Sep 29 2023 at 08:57)
• Main developer of coq_makefile (9 messages, latest: Sep 28 2023 at 13:50)
• test suite timeouts in CI (4 messages, latest: Sep 27 2023 at 21:12)
• [CI] deriving (1 message, latest: Sep 25 2023 at 07:16)
• Situation of async interruptions (17 messages, latest: Sep 22 2023 at 16:51)
• Sort polymorphism plans (5 messages, latest: Sep 22 2023 at 10:20)
• CI timeout in "preparing" step (1 message, latest: Sep 21 2023 at 13:34)
• 8.18.0 Docker (48 messages, latest: Sep 21 2023 at 12:45)
• Error: Native compiler failed with error: Cannot allocate me (1 message, latest: Sep 20 2023 at 21:54)
• Roadmap (8 messages, latest: Sep 20 2023 at 15:51)
• Coq Call September 19th (1 message, latest: Sep 19 2023 at 20:03)
• 8.18 documentation (6 messages, latest: Sep 18 2023 at 13:19)
• 8.16 is the "latest" version in Coq platform (4 messages, latest: Sep 18 2023 at 05:18)
• rewrite opacity (5 messages, latest: Sep 15 2023 at 01:47)
• insufficient types (7 messages, latest: Sep 14 2023 at 17:58)
• Conditional compilation with version number (5 messages, latest: Sep 14 2023 at 15:13)
• external libraries and upstream Coq (18 messages, latest: Sep 14 2023 at 05:45)
• flambda (6 messages, latest: Sep 13 2023 at 16:21)
• dev/shim/coqtop (15 messages, latest: Sep 13 2023 at 08:52)
• ✔ dev/shim/coqtop inconsistent assumptions (6 messages, latest: Sep 12 2023 at 18:06)
• ci-template vs ci-template-flambda (3 messages, latest: Sep 11 2023 at 20:12)
• Why are some `.v` files listed as executable in the stdlib? (3 messages, latest: Sep 11 2023 at 20:10)
• dev/shim/coqtop inconsistent assumptions (1 message, latest: Sep 11 2023 at 16:01)
• ✔ V8.18.0 tag (5 messages, latest: Sep 10 2023 at 21:09)
• stressing the native compiler on the bench (6 messages, latest: Sep 09 2023 at 16:23)
• V8.18.0 tag (16 messages, latest: Sep 08 2023 at 09:54)
• Coq Call September 5th (22 messages, latest: Sep 07 2023 at 14:58)
• Timeouts in the CI (22 messages, latest: Sep 07 2023 at 10:26)
• OPAM for 8.18+rc1 (40 messages, latest: Sep 06 2023 at 12:53)
• docker image MIA (20 messages, latest: Sep 06 2023 at 12:41)
• stage of warnings option (1 message, latest: Sep 05 2023 at 10:23)
• Background diff tag hack (4 messages, latest: Sep 04 2023 at 21:34)
• Constr.decompose_app (6 messages, latest: Sep 04 2023 at 14:44)
• Maintenance teams in need of maintainers (2 messages, latest: Sep 04 2023 at 13:17)
• Trying to remove Int31 in Numbers/Cyclic (2 messages, latest: Sep 04 2023 at 12:53)
• make ci-jasmin (locally) (8 messages, latest: Sep 03 2023 at 15:28)
• Checks tab message (2 messages, latest: Sep 03 2023 at 08:28)
• Power cut apparently impacting CI on 2 Sep 2023 (5 messages, latest: Sep 02 2023 at 10:34)
• docker-boot failure (2 messages, latest: Aug 31 2023 at 13:47)
• 403 in CI (8 messages, latest: Aug 29 2023 at 06:35)
• Github extremely slow today? (14 messages, latest: Aug 28 2023 at 09:54)
• PR in need of review & assignee (2 messages, latest: Aug 26 2023 at 01:21)
• 8.18 (3 messages, latest: Aug 25 2023 at 11:00)
• Formatting query results: About (5 messages, latest: Aug 24 2023 at 07:37)
• Question on VERNAC EXTEND API & parsing/exec separation (23 messages, latest: Aug 23 2023 at 13:58)
• inconsistent assumptions (3 messages, latest: Aug 23 2023 at 04:23)
• Turning a coq plugin to a library (11 messages, latest: Aug 22 2023 at 18:50)
• ✔ Trivial PR fixing CI (2 messages, latest: Aug 22 2023 at 09:20)
• Trivial PR fixing CI (2 messages, latest: Aug 22 2023 at 07:45)
• Website down? (101 messages, latest: Aug 20 2023 at 17:02)
• ✔ Coq Package Index & core-dev suite (7 messages, latest: Aug 20 2023 at 09:38)
• Equations tag for 8.18 (39 messages, latest: Aug 19 2023 at 14:04)
• Type of values for primitives (9 messages, latest: Aug 19 2023 at 08:54)
• Number notation and custom entries? (8 messages, latest: Aug 09 2023 at 14:28)
• installing without sphinx? (9 messages, latest: Aug 08 2023 at 16:35)
• ✔ Changes to Declarations.universes from Coq 8.9 to 8.10 (4 messages, latest: Aug 07 2023 at 20:40)
• Changes to Declarations.universes from Coq 8.9 to 8.10 (4 messages, latest: Aug 07 2023 at 19:24)
• sketchy build errors (6 messages, latest: Aug 06 2023 at 07:33)
• native stack overflow (2 messages, latest: Aug 05 2023 at 23:05)
• smtcoq conflicts with #17875 (1 message, latest: Aug 05 2023 at 16:14)
• performance of lazy on primitive floats (1 message, latest: Aug 05 2023 at 03:28)
• PR before 8.18.0 (1 message, latest: Aug 05 2023 at 01:39)
• build broken (3 messages, latest: Aug 04 2023 at 19:57)
• milestones (1 message, latest: Aug 02 2023 at 15:39)
• OCaml 5 performance (8 messages, latest: Aug 02 2023 at 07:56)
• roadmap (26 messages, latest: Aug 01 2023 at 07:43)
• Evarconv.unify as an Ltac2 primitive (22 messages, latest: Jul 31 2023 at 19:45)
• Intros' error message (3 messages, latest: Jul 31 2023 at 16:15)
• Mac failing to build plugins? (32 messages, latest: Jul 29 2023 at 04:02)
• Avoiding running the vm / native compiler twice (37 messages, latest: Jul 28 2023 at 16:00)
• Warning 8 (16 messages, latest: Jul 28 2023 at 15:37)
• Untracked files (2 messages, latest: Jul 28 2023 at 15:23)
• Fixing bug #17833 (3 messages, latest: Jul 27 2023 at 22:13)
• ✔ Moving from Name.t to Context.binder_annot (4 messages, latest: Jul 25 2023 at 19:50)
• Inconsistency (19 messages, latest: Jul 22 2023 at 10:35)
• Poll on non-associative notations (49 messages, latest: Jul 22 2023 at 06:50)
• platform failing in CI (windows) (9 messages, latest: Jul 21 2023 at 08:52)
• Why is unification right-to-left? (7 messages, latest: Jul 20 2023 at 21:26)
• ✔ From opaque back to constr (3 messages, latest: Jul 17 2023 at 19:19)
• From opaque back to constr (1 message, latest: Jul 17 2023 at 18:55)
• ✔ Replacement for Goal.V82.abstract_type (1 message, latest: Jul 17 2023 at 18:45)
• what is ocamlopt status 2? (11 messages, latest: Jul 17 2023 at 18:29)
• native_compute success story (1 message, latest: Jul 17 2023 at 04:36)
• Replacement for Goal.V82.abstract_type (3 messages, latest: Jul 14 2023 at 20:09)
• Presence or availability for the 2023 Coq Workshop (5 messages, latest: Jul 12 2023 at 13:50)
• ✔ Using PG from the Coq repo (13 messages, latest: Jul 12 2023 at 12:43)
• Coq 8.17.1 (115 messages, latest: Jul 12 2023 at 12:17)
• Changes to simpl in 8.18? (16 messages, latest: Jul 10 2023 at 09:34)
• Fall 2023 Coq Hackaton (3 messages, latest: Jul 07 2023 at 13:26)
• Coq regression observed with MathComp-Analysis (24 messages, latest: Jul 06 2023 at 12:20)
• runner failures (3 messages, latest: Jul 05 2023 at 13:50)
• ✔ Ocaml-lsp unbound module error (3 messages, latest: Jul 04 2023 at 16:32)
• Ocaml-lsp unbound module error (21 messages, latest: Jul 04 2023 at 15:59)
• CI, Docker, Dependencies (19 messages, latest: Jul 04 2023 at 12:23)
• OCaml warnings 67 and 69 (7 messages, latest: Jul 03 2023 at 19:57)
• opam packages for new releases (10 messages, latest: Jun 30 2023 at 16:07)
• Instruction counts PR (9 messages, latest: Jun 27 2023 at 12:19)
• tactic implementation (3 messages, latest: Jun 27 2023 at 09:35)
• Waterproof becomes a plugin (3 messages, latest: Jun 21 2023 at 12:43)
• hb_test failing in CI (12 messages, latest: Jun 20 2023 at 11:04)
• Reproduce opam-coq-archive CI (3 messages, latest: Jun 19 2023 at 15:58)
• Ltac2 abstract and evars (3 messages, latest: Jun 19 2023 at 10:37)
• Branch rulesets (39 messages, latest: Jun 12 2023 at 13:29)
• inductives implicitly Prop and template poly (4 messages, latest: Jun 09 2023 at 23:27)
• CI broken (output test failure) (4 messages, latest: Jun 09 2023 at 13:58)
• CI infrastructure (30 messages, latest: Jun 09 2023 at 07:55)
• Help with opam package (8 messages, latest: Jun 07 2023 at 12:12)
• base+async CI broken on master? (2 messages, latest: Jun 05 2023 at 11:30)
• Dune, coqtop, and native_compute (5 messages, latest: Jun 05 2023 at 09:53)
• itauto broken (28 messages, latest: Jun 05 2023 at 07:20)
• CoqIDE future (102 messages, latest: Jun 02 2023 at 13:46)
• document people to contact for CI projects (9 messages, latest: Jun 02 2023 at 13:01)
• perennial warnings as error (7 messages, latest: Jun 02 2023 at 12:58)
• Issues about extraction (36 messages, latest: May 31 2023 at 14:14)
• globalize0 behaviour (1 message, latest: May 30 2023 at 10:41)
• the definition of structurally smaller (11 messages, latest: May 27 2023 at 05:15)
• reduction options (2 messages, latest: May 25 2023 at 14:45)
• geocoq failing in bench (4 messages, latest: May 17 2023 at 11:28)
• Only printing abbreviations (18 messages, latest: May 17 2023 at 10:00)
• mathcomp failing (7 messages, latest: May 11 2023 at 10:58)
• github bugging out (2 messages, latest: May 09 2023 at 11:46)
• LFA (3 messages, latest: May 05 2023 at 10:51)
• -beautify (3 messages, latest: May 01 2023 at 21:38)
• spurious quickchick failures (4 messages, latest: May 01 2023 at 14:49)
• cancelled CI runs (2 messages, latest: Apr 28 2023 at 20:49)
• ✔ ci-coq_library_undecidability and PR #17538 (1 message, latest: Apr 28 2023 at 09:07)
• ci-coq_library_undecidability and PR #17538 (4 messages, latest: Apr 28 2023 at 08:29)
• rewrite_strat orderings? (1 message, latest: Apr 28 2023 at 07:08)
• Coq Release 8.17 (246 messages, latest: Apr 27 2023 at 13:43)
• ✔ Legacy unification semantics (11 messages, latest: Apr 27 2023 at 11:30)
• open recursion pretyper (1 message, latest: Apr 26 2023 at 19:04)
• Qed performance vs Defined (4 messages, latest: Apr 25 2023 at 21:23)
• Libobject and proofs (20 messages, latest: Apr 22 2023 at 22:18)
• Constr Cast (3 messages, latest: Apr 19 2023 at 12:24)
• STM deprecation (65 messages, latest: Apr 19 2023 at 09:11)
• IDProp vs True (14 messages, latest: Apr 18 2023 at 12:47)
• Dnylink Error when trying to add merlin-lib as dependency (4 messages, latest: Apr 18 2023 at 08:09)
• Documentation for ".mlg" file syntax (25 messages, latest: Apr 17 2023 at 14:45)
• package browsing website (3 messages, latest: Apr 17 2023 at 09:09)
• tactics in terms and typeclasses (9 messages, latest: Apr 14 2023 at 01:18)
• intros quiz (5 messages, latest: Apr 13 2023 at 15:36)
• ✔ Not the right number of induction arguments (3 messages, latest: Apr 11 2023 at 03:56)
• Formatting OCaml Contributions (7 messages, latest: Apr 10 2023 at 19:23)
• `Reduction.whd_all` (2 messages, latest: Apr 07 2023 at 08:57)
• polymorphic equivalent of constr_of_monomorphic_global (7 messages, latest: Apr 04 2023 at 14:51)
• testing delayed constraints (1 message, latest: Apr 04 2023 at 12:25)
• ✔ Installing coq-stdlib with opam (15 messages, latest: Apr 04 2023 at 10:24)
• Issues building 8.17.0 on Windows (20 messages, latest: Apr 04 2023 at 08:11)
• Installing coq-stdlib with opam (24 messages, latest: Apr 03 2023 at 20:59)
• Hints.FullHint.pattern, replacement? (78 messages, latest: Mar 31 2023 at 14:25)
• Detecting Stdlib installation (12 messages, latest: Mar 31 2023 at 08:08)
• Haskell extraction performance issue (8 messages, latest: Mar 30 2023 at 15:59)
• vst broken in CI (8 messages, latest: Mar 30 2023 at 12:05)
• "structural integrity problem" in CI (5 messages, latest: Mar 29 2023 at 15:22)
• misc/15933 CI failures (1 message, latest: Mar 29 2023 at 15:08)
• Serapi overlay & coq-lsp (9 messages, latest: Mar 29 2023 at 09:41)
• ✔ Serapi overlay & coq-lsp (7 messages, latest: Mar 29 2023 at 06:47)
• 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)
• Finding all locations where a definition is unfolded (12 messages, latest: Mar 22 2023 at 17:08)
• ✔ difference between 8.4 and 8.5 docker images? (6 messages, latest: Mar 20 2023 at 21:14)
• difference between 8.4 and 8.5 docker images? (3 messages, latest: Mar 20 2023 at 20:56)
• -fake-source (27 messages, latest: Mar 19 2023 at 23:50)
• 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)
• 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)
• 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)
• 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)
• 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)
• 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)
• `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)
• 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)
• 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)
• 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)
• 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)
• 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: Oct 08 2024 at 14:01 UTC