index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2021-04-01
[build] [ocamldebug] Update for byterun -> coqrun renaming
Emilio Jesus Gallego Arias
2021-04-01
Merge PR #14039: [dune] Rename byterun to coqrun
coqbot-app[bot]
2021-04-01
Merge PR #14030: [doc] [dune] Some tweaks from #13617
coqbot-app[bot]
2021-04-01
[doc] [dune] Some tweaks from #13617
Emilio Jesus Gallego Arias
2021-04-01
Merge PR #14047: [ci] Disable native compilation for paramcoq
coqbot-app[bot]
2021-04-01
Merge PR #14044: [RM] changelog for 8.13.2
coqbot-app[bot]
2021-04-01
[ci] Disable native compilation for paramcoq
Emilio Jesus Gallego Arias
2021-04-01
Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ...
coqbot-app[bot]
2021-04-01
Update doc/sphinx/changes.rst
Enrico Tassi
2021-04-01
Update doc/sphinx/changes.rst
Enrico Tassi
2021-04-01
changelog for 8.13.2
Enrico Tassi
2021-03-31
[dune] Rename byterun to coqrun
Emilio Jesus Gallego Arias
2021-03-31
Merge PR #14035: Fix printing of ssr do intros and seq tactics
coqbot-app[bot]
2021-03-31
Fix printing of ssr do intros and seq tactics
Lasse Blaauwbroek
2021-03-31
Merge PR #14033: Properly expand projection parameters in Btermdn.
coqbot-app[bot]
2021-03-31
Merge PR #14022: Replace mentions of Num by Zarith.
coqbot-app[bot]
2021-03-30
Merge PR #11791: [flags] [profile] Remove bitrotten CProfile calls.
Pierre-Marie Pédrot
2021-03-30
Properly expand projection parameters in Btermdn.
Pierre-Marie Pédrot
2021-03-30
[flags] [profile] Remove bit-rotten CProfile code.
Emilio Jesus Gallego Arias
2021-03-30
Merge PR #14012: Fix Ltac2 `Array.init` exponential overhead
Pierre-Marie Pédrot
2021-03-30
Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.
Pierre-Marie Pédrot
2021-03-30
Merge PR #13958: [recordops] complete API rewrite; the module is now called [...
Pierre-Marie Pédrot
2021-03-30
Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.
Michael Soegtrop
2021-03-29
[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0
Emilio Jesus Gallego Arias
2021-03-29
Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:...
coqbot-app[bot]
2021-03-29
Merge PR #14025: [coqdep] remove leftover Caml stuff from man page
coqbot-app[bot]
2021-03-29
Added a changelog.
Pierre-Marie Pédrot
2021-03-28
[coqdep] remove leftover Caml stuff from man page
Hendrik Tews
2021-03-28
Replace mentions of Num by Zarith.
Guillaume Melquiond
2021-03-26
Merge PR #11907: [zify] attempt to speed up look up of constr
Pierre-Marie Pédrot
2021-03-26
[doc] cleanup pretyping/structures.mli
Enrico Tassi
2021-03-26
Add non-performance-based test
Jason Gross
2021-03-26
Add an Ltac1 to Ltac2 FFI for identifiers.
Pierre-Marie Pédrot
2021-03-26
[ci] overlay file for #13958
Enrico Tassi
2021-03-26
[recordops] complete API rewrite; the module is now called [structures]
Enrico Tassi
2021-03-26
Document as critical.
Guillaume Melquiond
2021-03-26
Be more thorough when testing PArray.set.
Guillaume Melquiond
2021-03-26
Improve dump of primitive OCaml operations.
Guillaume Melquiond
2021-03-26
Support OCaml primitives with an actual arity larger than 4.
Guillaume Melquiond
2021-03-26
Make it more obvious when the calling convention of APPLY changes.
Guillaume Melquiond
2021-03-26
Fix assertion that checks that APPLY can only be passed 4 arguments.
Guillaume Melquiond
2021-03-26
Split the return type away from the signature of primitive operations.
Guillaume Melquiond
2021-03-26
Merge PR #14007: Never store persistent arrays as VM structured values.
coqbot-app[bot]
2021-03-26
Fix Ltac2 `Array.init` exponential overhead
Jason Gross
2021-03-26
Adding a changelog.
Pierre-Marie Pédrot
2021-03-26
Similar fix for native compilation.
Pierre-Marie Pédrot
2021-03-26
Never store persistent arrays as VM structured values.
Pierre-Marie Pédrot
2021-03-26
remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid
Andrej Dudenhefner
2021-03-26
Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmas
coqbot-app[bot]
2021-03-25
Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.
coqbot-app[bot]
[next]