aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-03-09Remove some productionlistsJim Fehrle
2020-03-08[doc] [dune] Update Dune build instructionsEmilio Jesus Gallego Arias
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
2020-02-28Merge PR #11423: Convert Vernacular section of gallina chapter to use prodnThéo Zimmermann
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-28Adapt the documentation after deprecation of term hints.Pierre-Marie Pédrot
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
2020-02-27Fix #11696: link from refman to stdlib doc is dead.Théo Zimmermann
2020-02-24Make it clear how to import Ltac2Clément Pit-Claudel
2020-02-24added sphinx docAbhishek Anand (optiplex7010@home)
2020-02-23Merge PR #11120: Refactoring code for application printing + fixing #11091 (i...Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:07:56 +0000