aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/gallina-specification-language.rst
AgeCommit message (Expand)Author
2019-04-02Allow underscores as comments in numeral constants.Pierre Roux
2019-04-02Update documentationPierre Roux
2019-03-18[Manual] Parametrize -> ParametErizeLysxia
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-19Fix typo in gallina specification language docyudetamago
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
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-17Add missing index entries.Théo Zimmermann
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-12Tactic deprecation machineryMaxime Dénès
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-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
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
2018-05-28Improve sections on (Co)Fixpoint of the Gallina chapter.Théo Zimmermann
2018-05-27Improve subsection on co-inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Improve subsection on mutual inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Move 'new in Coq 8.1' subsection to an appropriate place.Théo Zimmermann
2018-05-27Document Variant properly.Théo Zimmermann
2018-05-27Improve inductive types subsection of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Definitions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Assumptions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve the section Terms of the Gallina chapter.Théo Zimmermann
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
2018-05-21Document the new nested-proof error message.Théo Zimmermann
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-14Remove duplicate entries for Proof, Qed, Defined, Admitted.Théo Zimmermann
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-14[Sphinx] Fix all remaining warnings.Maxime Dénès
2018-04-14[sphinx] Fix many warnings.Théo Zimmermann
2018-04-13[Sphinx] Add Chapter 1Maxime Dénès
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:50:19 +0000