aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-07Merge PR #14056: Miscellaneous mini-"typos" fixescoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: silene
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-06Add a relative link to coq-core.Théo Zimmermann
2021-04-06Typo in ChoiceFacts.Hugo Herbelin
2021-04-06Missing dot in an error message.Hugo Herbelin
2021-04-06One catch-all's missing a noncritical; another is now useless (see 7efaf86).Hugo Herbelin
2021-04-06Standardizing spacing for {| ... |} in two files.Hugo Herbelin
2021-04-06Typo in a micromega comment.Hugo Herbelin
2021-04-06Uniformizing the "already exists" messagesHugo Herbelin
2021-04-06Make description of Pp.pr_enum more precise + spacing in pp.ml.Hugo Herbelin
2021-04-06CI-paramcoq: Re-enable nativeGaëtan Gilbert
It's an issue in paramcoq's test suite, which doesn't respect COQEXTRAFLAGS and so will be handled upstream (https://github.com/coq-community/paramcoq/pull/66)
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-06Add odoc warnings for empty packages.Théo Zimmermann
From an OCaml library point of view.
2021-04-06Remove unused UnivProblem.Set.subst_univsGaëtan Gilbert
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-02Fixes #11690: wrongly toggled coqide printing matching flag; moving raw->nested.Hugo Herbelin
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
add polynomial specifications of to_nat add changelog and doc entries
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-31[dune] [coqdoc] Install coqdoc.sty also in share/texmfEmilio Jesus Gallego Arias
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-30Remove the :> type castJim Fehrle
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:42:16 +0000