aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-16Print Universes SubgraphGaëtan Gilbert
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-10-29Fix typos in the document about CICwkwkes
2018-10-23Order Greek letters consistently w/rest of documentSam Pablo Kuper
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-10-10Merge PR #8384: Small fixes in attribute documentation.Clément Pit-Claudel
2018-10-01Docs: Missing backquoteJoachim Breitner
2018-09-28Small fixes in attribute documentation.Théo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
2018-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-17Add missing index entries.Théo Zimmermann
2018-09-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
2018-08-16Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examplesMaxime Dénès
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
2018-07-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' o...Zeimer
2018-07-19Fixed some typos and grammar errors from section 'The language' of the Refere...Zeimer
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-04doc: Fix markup in Calculus of Inductive ConstructionsFabian
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-29doc: Fix typesetting in Gallina extensionsLysxia
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Update gallina-extensions.rstAmbroise
2018-06-24Documenting the syntax of mutual keywords.Pierre-Marie Pédrot
2018-06-16[sphinx] Finish clean-up of the Canonical Structure subsection.Théo Zimmermann
2018-06-16doc: Add "Print Canonical Projections" command to Command indexAnton Trunov
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-05-28Improve the last section of the Gallina chapter.Théo Zimmermann
2018-05-28Chapter 1 of the refman compiles without reporting any undocumented object.Théo Zimmermann