aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-02-02Merge PR #11466: checkdeps.py: add missing dep & report deps all at onceThéo Zimmermann
2020-01-30Merge PR #11464: Fix off-by-one in docs of `first num last` (fix #11463)Enrico Tassi
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2020-01-27Rephrase to reduce ambiguityPaolo G. Giarrusso
2020-01-27Fix off-by-one in docs of `first num last` (fix #11463)Paolo G. Giarrusso
2020-01-27checkdeps.py: report *all* missing dependencies at oncePaolo G. Giarrusso
2020-01-27checkdeps: check for sphinxcontrib-bibtexPaolo G. Giarrusso
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-23More minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-23Add missing 'and'.Théo Zimmermann
2020-01-22Minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Fix typo in changelog entry.Théo Zimmermann
2020-01-22Insert changelog entry for #11430 from v8.11 branch.Théo Zimmermann
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-22A few edits to the 8.11 section of the Changes chapter.Théo Zimmermann
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-21Merge PR #11425: Miscellaneous typosThéo Zimmermann
2020-01-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
2020-01-19Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors co...Pierre-Marie Pédrot
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-17Remove the CoqIDE "Revert all Buffers" command.Pierre-Marie Pédrot
2020-01-17Remove the Tactic menu from CoqIDE.Pierre-Marie Pédrot
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-14Merge PR #11370: [zify] elim let in MLPierre-Marie Pédrot
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...Hugo Herbelin
2020-01-14[zify] elim let in MLFrédéric Besson
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-11Merge PR #11349: [refman] [changelog] Announce omega replacement.Pierre-Marie Pédrot
2020-01-10missing spaceOlivier Laurent
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
2020-01-08Add changelog entry for native string extractionMaxime Dénès
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Add documentation for extraction of ascii and string literalsMaxime Dénès
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
2020-01-08Hide ExtrOcamlStringPlus.v like the other extraction filesXavier Leroy
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 18:14:45 +0000