aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-22Merge PR #11422: Fix #11421 computation of Set+2Pierre-Marie Pédrot
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-22Merge PR #11433: [xml-protocol doc] Fix link to vscoqHugo Herbelin
2020-01-21[xml-protocol doc] Fix link to vscoqRamkumar Ramachandra
2020-01-21More portable C flagsPierre Roux
2020-01-21Merge PR #11425: Miscellaneous typosThéo Zimmermann
2020-01-21Merge PR #11431: [ci] Pin SF until they solve their CI issues.Théo Zimmermann
2020-01-21[ci] Pin SF until they solve their CI issues.Emilio Jesus Gallego Arias
2020-01-21Translating a comment from French to English.Hugo Herbelin
2020-01-21Typo in an anomaly message.Hugo Herbelin
2020-01-21Typo in a comment of univ.mli.Hugo Herbelin
2020-01-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-20Merge PR #11411: Checker validation now performed over reified dataGaëtan Gilbert
2020-01-20Merge PR #11428: [mltop] Deprecate -load-ml options in anticipation of #11409Pierre-Marie Pédrot
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-20Dispatch code ownership of files in dev/doc.Théo Zimmermann
2020-01-19Merge PR #11406: [dune] [dbg] Add support for coqtop in dune-dbgGaëtan Gilbert
2020-01-19Merge PR #11214: Add a script to pin CI developments.Gaëtan Gilbert
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-19Merge PR #11348: Discharge inductive types without rechecking themPierre-Marie Pédrot
2020-01-19Removing text saying XML is future of PG, adding explicitly vscoq as a userHugo Herbelin
2020-01-17Merge PR #11413: [doc] [ltac2] Build Ltac2 documentationThéo Zimmermann
2020-01-17Merge PR #11410: [ci] [gitlab] Add `interruptible: true` to jobs.Théo Zimmermann
2020-01-17Add some more info to the maintainer doc.Théo Zimmermann
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17[doc] [ltac2] Build Ltac2 documentation [make build system]Emilio Jesus Gallego Arias
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
2020-01-17[dune] [dbg] Add support for coqtop in dune-dbgEmilio Jesus Gallego Arias
2020-01-17[ci] [gitlab] Add `interruptible: true` to jobs.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-16Merge PR #11400: Use the GTK completion widget in CoqIDEEmilio Jesus Gallego Arias
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-16Adding an option to change the autocompletion delay.Pierre-Marie Pédrot
2020-01-16Better handling of asynchronous completion.Pierre-Marie Pédrot
2020-01-16Hacking a completion widget based on the default GtkSourceView one.Pierre-Marie Pédrot
2020-01-16Move the per-architecture check of marshalled Uint63s to Values.Pierre-Marie Pédrot
2020-01-16Checker validation acts on object representations rather than objects.Pierre-Marie Pédrot
2020-01-16Code factorization in checker validation.Pierre-Marie Pédrot
2020-01-16[mltop] Remove error handling hacks in favor of default methods.Emilio Jesus Gallego Arias
2020-01-16[mltop] Store digest of modules used to compile files.Emilio Jesus Gallego Arias
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
2020-01-15Merge PR #11374: Close #11133Pierre-Marie Pédrot
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert