coq
coq copied to clipboard
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
The more precise location for Flags.warn is the past, ie it is deleted. Overlays: - https://github.com/rocq-prover/vscoq/pull/1086
We only need to mutate accus for cofix. Should be correct after https://github.com/rocq-prover/rocq/pull/20719
### Description of the problem I would have expected to see actual axioms, that is terms without a body. Instead, the internal proof details of orders on Q are revealed...
### Description of the problem The following code results in an unsatisfiable universe constraint, as we don't unify the `carrier default@{?i' ?j'}` solution with the expected Type generated by the...
This is an attempt to make changes in the algebraic hierarchy of mathcomp less painful. When a structure s with op1 and op2 is broken into s1 with op1 and...
Please take a look and let me know if I've gotten anything wrong. Thanks. @Janno? - [x] Added **changelog**.
We use the [thread-local-storage](https://github.com/c-cube/thread-local-storage) to store Rocq's imperative state on a per-thread basis. This enables multi-threading / multi-domain programming, and opens up many possibilities. Notes: - this is at RFC...
using https://guillaume.munch.name/software/ocaml/memprof-limits cc @gadmm
# Release checklist # ## When the release managers for version `X.X` get nominated ## - [x] Create a new issue to track the release process where you can copy-paste...
- a few small improvements - add comments in build system files - ~support dune for tuto0~ nevermind, dune gets confused https://gitlab.inria.fr/coq/coq/-/jobs/5787181 - add tuto4 for extending ltac2