index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2020-03-20
Build and install refman with Dune.
Théo Zimmermann
2020-03-19
Merge PR #11601: [refman] Move chapters into new structure.
Clément Pit-Claudel
2020-03-19
[declare] Bring more consistency to parameters using labels
Emilio Jesus Gallego Arias
2020-03-19
Merge 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#4983
Clément Pit-Claudel
2020-03-19
Interpret the Export modifier of Set and Unset as an attribute.
Théo Zimmermann
2020-03-19
Update fullGrammar, common.edit_mlg and orderedGrammar...
Théo Zimmermann
2020-03-19
Document all the existing attributes.
Théo Zimmermann
2020-03-19
Update fullGrammar and common.edit_mlg following #11839.
Théo Zimmermann
2020-03-19
Merge PR #11760: firstorder: default tactic is “auto with core”
Théo Zimmermann
2020-03-19
Adapt 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-19
Merge PR #11860: [ci] [docker] Update to 4.09.1
Gaëtan Gilbert
2020-03-19
Merge PR #11795: Print implicit arguments in types of references
Hugo Herbelin
2020-03-19
firstorder: default tactic is “auto with core”
Vincent Laporte
2020-03-18
[ci] [docker] Update to 4.09.1
Emilio Jesus Gallego Arias
2020-03-18
Merge PR #11559: Remove year in headers.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-18
Add documentation for the export hint.
Pierre-Marie Pédrot
2020-03-18
Merge PR #11746: Register commonly used names from the Reals library for plug...
Théo Zimmermann
2020-03-17
Merge PR #11811: Remove a positivity check when Positivity Checking is off
Gaëtan Gilbert
2020-03-16
Merge PR #11813: Fixed link to "match" syntax figures.
Théo Zimmermann
2020-03-16
Document coq_makefile behavior wrt -native-compiler yes
Pierre Roux
2020-03-14
Merge PR #10858: Implementing postponed constraints in TC resolution
Gaëtan Gilbert
2020-03-13
Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.
Emilio Jesus Gallego Arias
2020-03-13
Implementing postponed constraints in TC resolution
Matthieu Sozeau
2020-03-12
Merge PR #11796: Remove parallel building of Sphinx documentation.
Emilio Jesus Gallego Arias
2020-03-12
Update doc/sphinx/addendum/extended-pattern-matching.rst
larsr
2020-03-12
Fixed link to "match" syntax.
larsr
2020-03-12
Merge PR #11781: Minor improvements to the unreleased changelog.
Clément Pit-Claudel
2020-03-12
Merge PR #11780: Minor improvements to the unreleased changelog.
Clément Pit-Claudel
2020-03-12
Add changelog
SimonBoulier
2020-03-12
Dune build rules for doc_grammar and fullGrammar.
Théo Zimmermann
2020-03-12
Add changelog entry
SimonBoulier
2020-03-10
Remove parallel building of Sphinx documentation.
Théo Zimmermann
2020-03-09
Remove some productionlists
Jim Fehrle
2020-03-08
Minor improvements to the unreleased changelog.
Théo Zimmermann
2020-03-08
Minor improvements to the unreleased changelog.
Théo Zimmermann
2020-03-08
[doc] [dune] Update Dune build instructions
Emilio Jesus Gallego Arias
2020-03-08
Merge PR #11740: Ltac2: Add notation for enough and eenough
Pierre-Marie Pédrot
2020-03-05
Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.
Maxime Dénès
2020-03-05
Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...
Pierre-Marie Pédrot
2020-03-05
Merge PR #11602: Adding support for an "only parsing" modifier in "where"-bas...
Pierre-Marie Pédrot
2020-03-04
Fix #11749: don't warn for hidden files.
Théo Zimmermann
2020-03-04
Merge PR #11429: [zify] several efficiency enhancements
Vincent Laporte
2020-03-04
Adding support for an "only parsing" modifier in "where"-based notations.
Hugo Herbelin
2020-03-04
Add file to register names of reals library used by gappa
Michael Soegtrop
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2020-03-03
[zify] efficiency improvements
Frédéric Besson
[prev]
[next]