aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-06Add a relative link to coq-core.Théo Zimmermann
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
From an OCaml library point of view.
2021-04-05Merge PR #13624: Fixing #13581: missing support for let-ins in arity of ↵coqbot-app[bot]
inductive types for extraction Reviewed-by: pi8027
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04Adding change log for #13624.Hugo Herbelin
2021-04-04Fixing #13581: missing support for let-ins in arity of inductive types.Hugo Herbelin
At first view, the fix takes care about when to use the number of assumptions and when to also include local definitions, but I don't know all the details of the implementation to be absolutely sure.
2021-04-01Merge PR #14053: [build] [ocamldebug] Update for byterun -> coqrun renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01[build] [ocamldebug] Update for byterun -> coqrun renamingEmilio Jesus Gallego Arias
Addendum to #14039 .
2021-04-01Merge PR #14039: [dune] Rename byterun to coqruncoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01Merge PR #14030: [doc] [dune] Some tweaks from #13617coqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01[doc] [dune] Some tweaks from #13617Emilio Jesus Gallego Arias
Tweaks to docs that are independent / unrelated to that PR.
2021-04-01Merge PR #14047: [ci] Disable native compilation for paramcoqcoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
Reviewed-by: Zimmi48
2021-04-01[ci] Disable native compilation for paramcoqEmilio Jesus Gallego Arias
Paramcoq is typically flaky on our worker configuration, c.f. https://gitlab.com/coq/coq/-/jobs/1144081161
2021-04-01Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ↵coqbot-app[bot]
< 4.07.0 Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-31[dune] Rename byterun to coqrunEmilio Jesus Gallego Arias
This seems the official name, the byterun name is just an artifact from the very preliminary dune build.
2021-03-31Merge PR #14035: Fix printing of ssr do intros and seq tacticscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: ppedrot
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]
Reviewed-by: mattam82
2021-03-31Merge PR #14022: Replace mentions of Num by Zarith.coqbot-app[bot]
Reviewed-by: pi8027
2021-03-30Merge PR #11791: [flags] [profile] Remove bitrotten CProfile calls.Pierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections.
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
As of today Coq has the `CProfile` infrastructure disabled by default, untested, and not easily accessible. It was decided that `CProfile` should remain not user-accessible, and only available thus by manual editing of Coq code to switch the flag and manually instrument functions. We thus remove all bitrotten dead code.
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-30Merge PR #13958: [recordops] complete API rewrite; the module is now called ↵Pierre-Marie Pédrot
[structures] Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: herbelin Reviewed-by: ppedrot
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
Fixes #10704
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary ↵coqbot-app[bot]
dependencies: Le, Gt, Minus, Lt, Setoid Reviewed-by: anton-trunov
2021-03-29Merge PR #14025: [coqdep] remove leftover Caml stuff from man pagecoqbot-app[bot]
Reviewed-by: ejgallego
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-28[coqdep] remove leftover Caml stuff from man pageHendrik Tews
Dependencies for Caml files was removed in PR #11589, but some parts of it survived in the man page.
2021-03-28Replace mentions of Num by Zarith.Guillaume Melquiond
The documentation of extraction became outdated when the big.ml wrapper got modified by 094e4649c29e2426daca0476c140439de901dafe.
2021-03-26Merge PR #11907: [zify] attempt to speed up look up of constrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
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
Before you ask, the Ltac2.Ltac1 module is voluntarily underdocumented. Fixes #13996: missing Ltac1.to_ident.
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
PArray.set has arity 4, but due to the polymorphic universe, its actual arity is 5. As a consequence, Kshort_apply cannot be used to invoke it (or rather its accumulating version). Using Kapply does not quite work here, because Kpush_retaddr would have to be invoked before the arguments, that is, before we even know whether the arguments are accumulators. So, to use Kapply, one would need to push the return address, push duplicates of the already computed arguments, call the accumulator, and then pop the original arguments. This commit follows a simpler approach, but more restrictive, as it is still limited to arity 4, but this time independently from universes. To do so, the call is performed in two steps. First, a closure containing the universes is created. Second, the actual application to the original arguments is performed, for which Kshort_apply is sufficient. So, this is inefficient, because a closure is created just so that it can be immediately fully applied. But since this is the accumulator slow path, this does not matter.
2021-03-26Make it more obvious when the calling convention of APPLY changes.Guillaume Melquiond
Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments.
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
This avoids having to drop the last element of the signature in the common case.
2021-03-26Merge PR #14007: Never store persistent arrays as VM structured values.coqbot-app[bot]
Reviewed-by: silene
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:39:29 +0000