aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
2021-04-06Remove unused UnivProblem.Set.subst_univsGaëtan Gilbert
2021-04-06Merge PR #14042: Fix a bug in UnivProblemPierre-Marie Pédrot
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
2021-04-05Merge PR #13624: Fixing #13581: missing support for let-ins in arity of induc...coqbot-app[bot]
2021-04-04More extraction tests for inductive types with let-ins.Hugo Herbelin
2021-04-04[coqpp] Add -helpEmilio Jesus Gallego Arias
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
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
2021-04-01Merge PR #14053: [build] [ocamldebug] Update for byterun -> coqrun renamingcoqbot-app[bot]
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-04-01Fix a bug in UnivProblemMatthieu Sozeau
2021-03-31[dune] Rename byterun to coqrunEmilio Jesus Gallego Arias
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]
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-30CI: don't output-syncGaëtan Gilbert
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-29Print type of offending expression in Ltac2 not-unit warning.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 02:56:36 +0000