aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-02-13Merge PR #11098: Let Arguments support anonymous implicit argumentsEmilio Jesus Gallego Arias
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-11Update doc/sphinx/practical-tools/utilities.rstJason Gross
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-11Merge PR #11235: Add syntax for non maximal implicit argumentsHugo Herbelin
2020-02-08Remove -compat 8.9.Théo Zimmermann
2020-02-08Merge PR #11240: Add rew dependent NotationsHugo Herbelin
2020-02-08Merge PR #10343: Resolve 10342 : [Ltac2] Add array libraryPierre-Marie Pédrot
2020-02-08Merge PR #11404: replace RList by list R in all files where it is used in thi...Pierre-Marie Pédrot
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-07[coqdep] Add changelog for recent modifications.Emilio Jesus Gallego Arias
2020-02-06Apply suggestions from code reviewJason Gross
2020-02-06replace RList by list RYves Bertot
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
2020-02-04Apply suggestions from HugoSimonBoulier
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 22:05:11 +0000