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-01-17
Remove the CoqIDE "Revert all Buffers" command.
Pierre-Marie Pédrot
2020-01-17
Remove the Tactic menu from CoqIDE.
Pierre-Marie Pédrot
2020-01-16
Adding a changelog.
Pierre-Marie Pédrot
2020-01-14
Merge PR #11370: [zify] elim let in ML
Pierre-Marie Pédrot
2020-01-14
Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...
Hugo Herbelin
2020-01-14
[zify] elim let in ML
Frédéric Besson
2020-01-14
[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorations
Karl Palmskog
2020-01-14
Document the Set Default Proof Mode command.
Pierre-Marie Pédrot
2020-01-14
Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...
Kazuhiko Sakaguchi
2020-01-13
Native compute: cleanup temporary files on program exit
Gaëtan Gilbert
2020-01-13
Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...
Pierre-Marie Pédrot
2020-01-11
Merge PR #11349: [refman] [changelog] Announce omega replacement.
Pierre-Marie Pédrot
2020-01-10
missing space
Olivier Laurent
2020-01-09
Merge PR #11164: [CS] allow Let variable to be canonical
Pierre-Marie Pédrot
2020-01-08
Add Set NativeCompute Timing
Jason Gross
2020-01-08
Add note about default goal selector next to bullet docs
Gaëtan Gilbert
2020-01-08
Add changelog entry for native string extraction
Maxime Dénès
2020-01-08
Factorize ascii extraction in ExtrOcamlChar.v
Maxime Dénès
2020-01-08
Add documentation for extraction of ascii and string literals
Maxime Dénès
2020-01-08
Rename ExtrOcamlStringPlus into ExtrOcamlNativeString
Xavier Leroy
2020-01-08
Hide ExtrOcamlStringPlus.v like the other extraction files
Xavier Leroy
2020-01-08
[refman] [changelog] Announce omega replacement.
Théo Zimmermann
2020-01-08
Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
SimonBoulier
2020-01-08
Trailing implicit: Maxime's suggestions
SimonBoulier
2020-01-07
Merge PR #11245: [tools] Remove support for python2
Théo Zimmermann
2020-01-07
Merge PR #11369: [refman] Correct manual about implicit parameters in inductives
Théo Zimmermann
2020-01-07
Correct manual about implicit parameters in inductives.
SimonBoulier
2020-01-07
Trailing implicit error: documentation
SimonBoulier
2020-01-07
Trailing implicit error: changelog
SimonBoulier
2020-01-06
doc: mention limitation of bidi hints vs program
Gaëtan Gilbert
2020-01-06
[micromega] fix of bug #11191
Frédéric Besson
2020-01-06
Merge PR #11361: Fix #11360: discharge of template inductive with param only ...
Pierre-Marie Pédrot
2020-01-06
Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migra...
Clément Pit-Claudel
2020-01-06
stdlib List: add [remove'] and [count_occ']
Yishuai Li
2020-01-06
Fix #11360: discharge of template inductive with param only use of var
Gaëtan Gilbert
2020-01-03
Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issue
Enrico Tassi
2020-01-03
coq_makefile: don't use CAMLPKGS when building cmxa of mllib
Gaëtan Gilbert
2020-01-03
[tools] Remove support for python2
Emilio Jesus Gallego Arias
2019-12-31
Merge PR #11325: [refman] Add missing s.
Pierre-Marie Pédrot
2019-12-30
Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...
Pierre-Marie Pédrot
2019-12-29
Remove :flag: that appears in the output
Jim Fehrle
2019-12-29
[refman] Fix bad quoting practice leftover from Sphinx migration.
Théo Zimmermann
2019-12-29
Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...
Théo Zimmermann
2019-12-29
Merge PR #11183: Enhance prodn in .rst doc files to support multiple producti...
Théo Zimmermann
2019-12-28
Prevent apostrophes and backticks from being stylized in latex
Jim Fehrle
2019-12-28
Convert productionlists to prodns
Jim Fehrle
2019-12-28
Update doc/sphinx/language/gallina-extensions.rst
Kazuhiko Sakaguchi
2019-12-28
Extend `Print Canonical Projections` with a search functionality
Kazuhiko Sakaguchi
2019-12-27
docs: Update changes.rst w.r.t. ssrsetoid.v's simplification
Erik Martin-Dorel
2019-12-26
Add rew dependent Notations
Jason Gross
[prev]
[next]