aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-04-01[build] [ocamldebug] Update for byterun -> coqrun renamingEmilio Jesus Gallego Arias
2021-04-01Merge PR #14039: [dune] Rename byterun to coqruncoqbot-app[bot]
2021-04-01Merge PR #14030: [doc] [dune] Some tweaks from #13617coqbot-app[bot]
2021-04-01[doc] [dune] Some tweaks from #13617Emilio Jesus Gallego Arias
2021-04-01Merge PR #14047: [ci] Disable native compilation for paramcoqcoqbot-app[bot]
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
2021-04-01[ci] Disable native compilation for paramcoqEmilio Jesus Gallego Arias
2021-04-01Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ...coqbot-app[bot]
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-31[dune] Rename byterun to coqrunEmilio Jesus Gallego Arias
2021-03-31Merge PR #14035: Fix printing of ssr do intros and seq tacticscoqbot-app[bot]
2021-03-31Fix printing of ssr do intros and seq tacticsLasse Blaauwbroek
2021-03-31Merge PR #14033: Properly expand projection parameters in Btermdn.coqbot-app[bot]
2021-03-31Merge PR #14022: Replace mentions of Num by Zarith.coqbot-app[bot]
2021-03-30Merge PR #11791: [flags] [profile] Remove bitrotten CProfile calls.Pierre-Marie Pédrot
2021-03-30Properly 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-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
2021-03-30Merge PR #13958: [recordops] complete API rewrite; the module is now called [...Pierre-Marie Pédrot
2021-03-30Merge 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.0Emilio Jesus Gallego Arias
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:...coqbot-app[bot]
2021-03-29Merge PR #14025: [coqdep] remove leftover Caml stuff from man pagecoqbot-app[bot]
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
2021-03-26Merge PR #11907: [zify] attempt to speed up look up of constrPierre-Marie Pédrot
2021-03-26[doc] cleanup pretyping/structures.mliEnrico Tassi
2021-03-26Add non-performance-based testJason Gross
2021-03-26Add an Ltac1 to Ltac2 FFI for identifiers.Pierre-Marie Pédrot
2021-03-26[ci] overlay file for #13958Enrico Tassi
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-26Document as critical.Guillaume Melquiond
2021-03-26Be more thorough when testing PArray.set.Guillaume Melquiond
2021-03-26Improve dump of primitive OCaml operations.Guillaume Melquiond
2021-03-26Support OCaml primitives with an actual arity larger than 4.Guillaume Melquiond
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
2021-03-26Fix assertion that checks that APPLY can only be passed 4 arguments.Guillaume Melquiond
2021-03-26Split the return type away from the signature of primitive operations.Guillaume Melquiond
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26Similar fix for native compilation.Pierre-Marie Pédrot
2021-03-26Never store persistent arrays as VM structured values.Pierre-Marie Pédrot
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
2021-03-25Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.coqbot-app[bot]