index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
[Sphinx] Move chapter 8 to new infrastructure
Maxime Dénès
2018-03-15
*
[Sphinx] Add chapter 5
Maxime Dénès
2018-03-15
*
[Sphinx] Move chapter 5 to new infrastructure
Maxime Dénès
2018-03-15
*
[Sphinx] Add chapter 4
Maxime Dénès
2018-03-15
*
[Sphinx] Move chapter 4 to new infrastructure
Maxime Dénès
2018-03-15
*
[Sphinx] Add chapter 2
Maxime Dénès
2018-03-15
*
[Sphinx] Move chapter 2 to new infrastructure
Maxime Dénès
2018-03-15
*
[Sphinx] Add credits
Maxime Dénès
2018-03-15
*
[Sphinx] Move credits to new infrastructure
Maxime Dénès
2018-03-15
*
[Sphinx] Add introduction
Maxime Dénès
2018-03-13
*
[Sphinx] Move introduction to new infrastructure
Maxime Dénès
2018-03-13
*
[Sphinx] Add "edit on github"
Maxime Dénès
2018-03-13
*
[Sphinx] Mention license
Maxime Dénès
2018-03-13
*
[Sphinx] Remove ad-hoc color for links interfering with TOC
Maxime Dénès
2018-03-13
*
[Sphinx] Update some metadata
Maxime Dénès
2018-03-13
*
[Sphinx] Read version number from configure
Maxime Dénès
2018-03-13
*
[Sphinx] Comment out metadata for unused backends
Maxime Dénès
2018-03-13
*
[Sphinx] Remove information for .chm backend
Maxime Dénès
2018-03-13
*
[Sphinx] add bibliography
Maxime Dénès
2018-03-13
*
[Sphinx] Add indexes
Maxime Dénès
2018-03-13
*
[Sphinx] Add table of contents
Maxime Dénès
2018-03-12
*
[Sphinx] Add doc preamble
Maxime Dénès
2018-03-12
*
[Sphinx] Add a few grammar constructions
Maxime Dénès
2018-03-12
*
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
|
*
Documentation for Cumulativity Weak Constraints.
Gaëtan Gilbert
2018-03-09
*
|
Merge PR #6480: Allow Prop as source for coercions
Maxime Dénès
2018-03-09
|
\
\
|
|
/
|
/
|
*
|
Merge PR #6818: Sphinx doc infrastructure
Maxime Dénès
2018-03-09
|
\
\
|
*
|
Moving Gitlab CI documentation build to the main Coq build.
Maxime Dénès
2018-03-09
|
*
|
Integration of a sphinx-based documentation generator.
Maxime Dénès
2018-03-09
*
|
|
Merge PR #6895: [compat] Remove "Refolding Reduction" option.
Maxime Dénès
2018-03-09
|
\
\
\
*
\
\
\
Merge PR #6820: Tacticals assert_fails and assert_succeeds
Maxime Dénès
2018-03-09
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
doc and changes for coercion from prop/type
charguer
2018-03-09
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6937: Add empty compat file for Coq 8.8
Maxime Dénès
2018-03-09
|
\
\
\
|
|
|
*
[compat] Remove "Refolding Reduction" option.
Emilio Jesus Gallego Arias
2018-03-08
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6909: Deprecate Focus and Unfocus
Maxime Dénès
2018-03-08
|
\
\
\
*
\
\
\
Merge PR #6582: Mangle auto-generated names
Maxime Dénès
2018-03-08
|
\
\
\
\
*
\
\
\
\
Merge PR #6903: [compat] Remove "Shrink Abstract"
Maxime Dénès
2018-03-08
|
\
\
\
\
\
|
|
|
|
*
|
Add empty compat file for Coq 8.8
Jason Gross
2018-03-07
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Remove outdated information regarding the FAQ.
Théo Zimmermann
2018-03-06
|
*
|
|
|
[compat] Remove "Shrink Abstract"
Emilio Jesus Gallego Arias
2018-03-06
|
/
/
/
/
*
|
|
|
Merge PR #6896: [compat] Remove NOOP deprecated options.
Maxime Dénès
2018-03-06
|
\
\
\
\
*
\
\
\
\
Merge PR #6824: Remove deprecated options related to typeclasses.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
|
|
|
|
|
*
|
Deprecate Focus and Unfocus.
Théo Zimmermann
2018-03-05
|
|
|
*
|
|
|
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
Remove deprecated options related to typeclasses.
Théo Zimmermann
2018-03-04
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-04
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #915: Fix rewrite in * side conditions
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
Fix typos.
Théo Zimmermann
2018-03-04
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
[next]
Maxime Dénès
Gaëtan Gilbert
charguer
Emilio Jesus Gallego Arias
Jason Gross
Théo Zimmermann