aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-08Gramlib: documentation of the recovery mechanism.Hugo Herbelin
2021-04-08Gramlib: some comments about how new rules are inserted.Hugo Herbelin
2021-04-08Gramlib: some comments about the main start/continue parsing loop.Hugo Herbelin
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
2021-04-06Merge PR #14042: Fix a bug in UnivProblemPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2021-04-06Merge PR #14063: Coqide: fixes #10720, highlight Variant keywordPierre-Marie Pédrot
2021-04-06Merge PR #14069: [coqpp] Add -helpPierre-Marie Pédrot
Reviewed-by: ppedrot
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-04[coqpp] Add -helpEmilio Jesus Gallego Arias
Closes #9932
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-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02Fixes #10720: highlighting Variant in CoqIDE.Hugo Herbelin
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-04-01Fix a bug in UnivProblemMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:12:27 +0000