aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-03-20Merge PR #11814: Document coq_makefile behavior wrt -native-compiler yesEnrico Tassi
2020-03-20Build and install refman with Dune.Théo Zimmermann
2020-03-19Merge PR #11601: [refman] Move chapters into new structure.Clément Pit-Claudel
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ...Théo Zimmermann
2020-03-19[refman] Stop using the deprecated math_block node (fixed GH-11856)Clément Pit-Claudel
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-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”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-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
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-18Merge PR #11746: Register commonly used names from the Reals library for plug...Théo Zimmermann
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
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-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
2020-03-13Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.Emilio Jesus Gallego Arias
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-12Merge PR #11796: Remove parallel building of Sphinx documentation.Emilio Jesus Gallego Arias
2020-03-12Update doc/sphinx/addendum/extended-pattern-matching.rstlarsr
2020-03-12Fixed link to "match" syntax. larsr
2020-03-12Merge PR #11781: Minor improvements to the unreleased changelog.Clément Pit-Claudel
2020-03-12Merge PR #11780: Minor improvements to the unreleased changelog.Clément Pit-Claudel
2020-03-12Add changelogSimonBoulier
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
2020-03-12Add changelog entrySimonBoulier
2020-03-10Remove parallel building of Sphinx documentation.Théo Zimmermann
2020-03-09Remove some productionlistsJim Fehrle
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-03-08[doc] [dune] Update Dune build instructionsEmilio Jesus Gallego Arias
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
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-05Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...Pierre-Marie Pédrot
2020-03-04Fix #11749: don't warn for hidden files.Théo Zimmermann
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-04Add file to register names of reals library used by gappaMichael Soegtrop
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:29:12 +0000