index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
sphinx
Age
Commit message (
Expand
)
Author
2020-04-29
Merge PR #11606: [tools] Add memory stats to tables by default
Emilio Jesus Gallego Arias
2020-04-29
Merge PR #12150: Support in-line glossary definitions and references with an ...
Clément Pit-Claudel
2020-04-29
Support in-line glossary entries and references
Jim Fehrle
2020-04-28
Merge PR #12183: Suggestion of improvement for the Allow SProp error message.
Gaëtan Gilbert
2020-04-28
Merge PR #11718: Convert syntax extensions chapter to prodn
Théo Zimmermann
2020-04-27
Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in...
Clément Pit-Claudel
2020-04-27
Merge PR #12132: [refman] Remove references to omega from Tactics chapter.
Vincent Laporte
2020-04-27
Further documentation improvements.
Théo Zimmermann
2020-04-27
Improve the Allow SProp error message.
Théo Zimmermann
2020-04-26
Convert syntax extensions chapter to prodn
Jim Fehrle
2020-04-26
Merge PR #12176: Doc: extend example for induction a bit
Théo Zimmermann
2020-04-25
Doc: extend example for induction a bit
Gaëtan Gilbert
2020-04-24
Add memory stats to tables by default
Jason Gross
2020-04-24
Merge PR #12156: Document `+` in polymorphic universe levels
Théo Zimmermann
2020-04-23
Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scope
Théo Zimmermann
2020-04-23
Merge PR #12117: Make multiplication of Cauchy reals transparent and accelera...
Hugo Herbelin
2020-04-23
[documentation] ssreflect: Abbreviations do not support scope
Kenji Maillard
2020-04-23
Merge PR #12148: Consolidate funind documentation onto a single page.
Clément Pit-Claudel
2020-04-23
[refman] Fix name of tactic: function induction -> functional induction.
Théo Zimmermann
2020-04-23
Fix coq snippets in Tactics chapter.
Théo Zimmermann
2020-04-23
Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...
Pierre-Marie Pédrot
2020-04-22
Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.
Hugo Herbelin
2020-04-22
Document Cauchy reals
Vincent Semeria
2020-04-22
Document `+` in polymorphic universe levels
Kenji Maillard
2020-04-21
Document changed warnings and erros following #12038.
Théo Zimmermann
2020-04-21
Move documentation on Funind into a single file.
Théo Zimmermann
2020-04-21
Merge all documentation on Funind into the same file.
Théo Zimmermann
2020-04-21
Consolidate funind tactics and Functional Scheme in Funind section of the Lib...
Théo Zimmermann
2020-04-21
Extract funind tactics to funind section of the Libraries chapter.
Théo Zimmermann
2020-04-21
Remove parts of the Tactics chapter.
Théo Zimmermann
2020-04-21
Remove parts of the Tactics chapter.
Théo Zimmermann
2020-04-21
Remove everything in the Tactics chapter up-to function induction and a bit b...
Théo Zimmermann
2020-04-20
[refman] Remove references to omega from Tactics chapter.
Théo Zimmermann
2020-04-20
TIMEFMT: Display the output file name
Jason Gross
2020-04-20
Remove funind tactics from Tactics chapter.
Théo Zimmermann
2020-04-20
Remove Functional Scheme from Scheme chapter.
Théo Zimmermann
2020-04-20
Move Functional Scheme to Funind section.
Théo Zimmermann
2020-04-20
Extract Functional Scheme from Scheme chapter.
Théo Zimmermann
2020-04-20
Remove probably useless doc/sphinx/coqdoc.css.
Théo Zimmermann
2020-04-19
CoqIDE: Adding a short documentation on style/theme customization.
Hugo Herbelin
2020-04-17
Deprecate “omega”
Vincent Laporte
2020-04-16
NativeCompute Timing: Use real, not user time
Jason Gross
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-04-13
Remove documentation for Hide menu in CoqIDE (was removed in 8.5).
Théo Zimmermann
2020-04-13
Update syntax of Import / Export in documentation.
Théo Zimmermann
2020-04-13
doc for partial imports
Gaëtan Gilbert
2020-04-11
Merge PR #11961: Convert vernac commands chapter to prodn, update syntax
Théo Zimmermann
2020-04-10
Convert vernac commands chapter to prodn, update syntax
Jim Fehrle
2020-04-09
Merge PR #11534: Support universe bindings and universe constraints in Let de...
Gaëtan Gilbert
2020-04-08
Merge PR #12005: Remove deprecated coqtop options
Emilio Jesus Gallego Arias
[next]