aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/gallina-extensions.rst
AgeCommit message (Expand)Author
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-22Merge PR #10178: Improve doc for generalizing bindersThéo Zimmermann
2019-05-22Improve doc for generalizing bindersGaëtan Gilbert
2019-05-19[refman] Fix up the grammar entry for field_defClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...Théo Zimmermann
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2019-05-10[refman] Mention the `#[canonical(false)]` attributeVincent Laporte
2019-04-30First fixing pass, and experiment with dune-style PR number and author listing.Théo Zimmermann
2019-03-25Fix indentationGan Shen
2019-03-25Update doc/sphinx/language/gallina-extensions.rstThéo Zimmermann
2019-03-24Fix typoGan Shen
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-13[refman] Fix Sphinx-translation regression in Arguments command.Théo Zimmermann
2019-03-13[refman] Remove warning silencing by fixing the underlying issue.Théo Zimmermann
2019-03-13[refman] Fix other newly emitted warnings.Théo Zimmermann
2019-03-12[refman] Add 'warn' option to coqtop directive.Théo Zimmermann
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-25[Manual] Document primitive integersVincent Laporte
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-13Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...Maxime Dénès
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-12Fix failing coqtops in gallina-extensions.rstGaëtan Gilbert
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
2019-01-23Clarify meaning of Primitive ProjectionsDavid A. Dalrymple
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...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-01Docs: Missing backquoteJoachim Breitner
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:06:07 +0000