index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Add bat files for 8.6rc1 build.
Maxime Dénès
2016-12-07
*
Add bat files for 8.6beta1 build.
Maxime Dénès
2016-12-07
*
Set version number to 8.6rc1.
Maxime Dénès
2016-12-07
*
A few words in CHANGES.
Maxime Dénès
2016-12-07
*
ssrmatching: fix iter_constr_LR iterator wrt Proj
Enrico Tassi
2016-12-07
*
Fix #5248 - test-suite fails in 8.6beta1
Maxime Dénès
2016-12-06
*
Fix broken documentation in presence of \zeroone{... \tt ...}.
Guillaume Melquiond
2016-12-06
*
Update documentation (bugs #5246 and #5251).
Guillaume Melquiond
2016-12-06
*
Merge remote-tracking branch 'github/pr/387' into v8.6
Maxime Dénès
2016-12-06
|
\
*
\
Merge remote-tracking branch 'github/pr/389' into v8.6
Maxime Dénès
2016-12-06
|
\
\
|
*
|
Change module for Coq loop
Paul Steckler
2016-12-05
|
*
|
the -byte option is deprecated
Paul Steckler
2016-12-05
|
/
/
|
*
ssrmatching: handle primite projections (fix: #5247)
Enrico Tassi
2016-12-05
*
|
Compute dependency of C files only in kernel/byterun.
Maxime Dénès
2016-12-05
|
/
*
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-04
|
\
*
\
Merge remote-tracking branch 'github/pr/378' into v8.6
Maxime Dénès
2016-12-04
|
\
\
*
|
|
Fix test-suite after change in "context" printing.
Maxime Dénès
2016-12-02
|
|
*
Document changes
Matthieu Sozeau
2016-12-02
*
|
|
Merge remote-tracking branch 'github/pr/377' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
*
\
\
\
Merge remote-tracking branch 'github/pr/372' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
*
\
\
\
\
Merge remote-tracking branch 'github/pr/368' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
*
\
\
\
\
\
Merge branch 'pr/367' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Fixing lexing of strings in comments for beautifier.
Hugo Herbelin
2016-12-02
|
*
|
|
|
|
|
Fixing printing of "ltac:" in tactics after surrounding parentheses
Hugo Herbelin
2016-12-02
|
|
|
|
|
*
|
Comment on universe handling in Parameters
Matthieu Sozeau
2016-12-02
|
|
|
|
|
*
|
Univs: fix bug #5188
Matthieu Sozeau
2016-12-02
*
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/381' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
*
|
|
|
|
|
|
|
Fix #5242 - Dubious unsilenceable warning on invalid identifier
Maxime Dénès
2016-12-02
|
|
*
|
|
|
|
|
Fixing printing of "Set Warnings Append".
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
Fixing space in printing "Context".
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
Fixing printers for pr_auto_using and pr_firstorder_using.
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
Fixing space in printing several list of implicit arguments.
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
Fixing printing of "only parsing" in abbreviations.
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
Protect printing of ltac's "context [...]" from possible collision
Hugo Herbelin
2016-12-02
|
|
*
|
|
|
|
|
More on fixing #5098 (preserving printing of "in hyp").
Hugo Herbelin
2016-12-02
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/380' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/369' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/371' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/364' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/382' into v8.6
Maxime Dénès
2016-12-02
|
\
\
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
|
[merlin] Adjust merlin for ide.
Emilio Jesus Gallego Arias
2016-11-30
|
/
/
/
/
/
/
/
/
/
/
/
|
|
|
|
|
*
|
|
|
|
|
Fix shelving order in typeclasses eauto.
Théo Zimmermann
2016-11-30
|
|
|
|
|
*
|
|
|
|
|
Fix typeclasses eauto shelving.
Théo Zimmermann
2016-11-30
|
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Fix bug #5232: proper globalization of hints paths
Matthieu Sozeau
2016-11-30
|
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
Univs: fix bug #5180
Matthieu Sozeau
2016-11-30
|
|
|
|
|
|
|
/
/
|
|
|
|
|
|
|
*
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
|
|
|
|
|
|
|
*
Slightly more efficient [Univ.super] implem
Matthieu Sozeau
2016-11-30
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Fix #5183 - Two CoqIDE crash errors
Maxime Dénès
2016-11-30
*
|
|
|
|
|
|
Update copyright on documentation cover.
Maxime Dénès
2016-11-30
*
|
|
|
|
|
|
Fix #5174: Underinformative syntax error messages in the new arguments syntax
Maxime Dénès
2016-11-30
[next]
Maxime Dénès
Enrico Tassi
Guillaume Melquiond
Paul Steckler
Matthieu Sozeau
Hugo Herbelin
Emilio Jesus Gallego Arias
Théo Zimmermann