aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-02-23Merge PR #11637: Update copyright in refman to year 2020.Clément Pit-Claudel
2020-02-23Documenting inheritance of implicit arguments and scopes in notations.Hugo Herbelin
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-19Update copyright in refman to year 2020.Théo Zimmermann
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
2020-02-17Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.Gaëtan Gilbert
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
2020-02-14Apply suggestions from code reviewJason Gross
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
2020-02-13[coqdep] Remove support for `-c` ocamldep replacement.Emilio Jesus Gallego Arias
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
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-06Apply suggestions from code reviewJason Gross
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
2020-02-04Apply suggestions from HugoSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-02-03Fix efficiency regression #11436Frédéric Besson
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-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-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-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 12:13:26 +0000