aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-03-27Remove the part about coqdoc from the utilities chapter.Théo Zimmermann
2020-03-27Prepare split of section about coqdoc.Théo Zimmermann
2020-03-26Merge PR #11929: Reintroduce a command that was actually used in another one....Clément Pit-Claudel
2020-03-26Reintroduce commands that were actually used. Fix build of PDF manual.Théo Zimmermann
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
2020-03-26CIC is printed in all-caps.Théo Zimmermann
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of co...Théo Zimmermann
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
2020-03-20Add an index for attributes.Théo Zimmermann
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ...Théo Zimmermann
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
2020-03-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-12Update doc/sphinx/addendum/extended-pattern-matching.rstlarsr
2020-03-12Fixed link to "match" syntax. larsr
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