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
*
coq_makefile: do not overwrite CAMLFLAGS
Enrico Tassi
2017-08-29
*
coq_makefile: use dedicated variable for extra packages
Enrico Tassi
2017-08-29
*
coq_makefile: build/use .cma for packed plugins
Enrico Tassi
2017-08-29
*
coq_makefile: test using findlib's package
Enrico Tassi
2017-08-29
*
test-suite: depend on byte compilation too
Enrico Tassi
2017-08-29
*
Merge PR #985: Fix coqdoc test-suite target on Windows.
Maxime Dénès
2017-08-29
|
\
*
|
Trying to fix deployment of master on bintray, and deploy tags to github.
Maxime Dénès
2017-08-29
*
|
Master now deploys 8.8+alpha.
Maxime Dénès
2017-08-29
*
|
Update .mailmap file.
Guillaume Melquiond
2017-08-24
|
*
Fix coqdoc URLs under Windows.
Théo Zimmermann
2017-08-21
|
*
Extend .gitignore for coqdoc test-suite.
Théo Zimmermann
2017-08-21
|
*
Fix coqdoc test-suite target on Windows.
Théo Zimmermann
2017-08-21
|
/
*
Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict wi...
Maxime Dénès
2017-08-18
|
\
*
\
Merge PR #983: Correct the option for cumulativity in CHANGES
Maxime Dénès
2017-08-18
|
\
\
*
\
\
Merge PR #973: Adding documentation for Printing Focused option.
Maxime Dénès
2017-08-18
|
\
\
\
|
|
*
|
Correct the option for cumulativity in CHANGES
Amin Timany
2017-08-18
*
|
|
|
Merge PR #801: Make Travis generate OSX packages.
Maxime Dénès
2017-08-18
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
Separate jobs for test-suite and package building under OSX.
Maxime Dénès
2017-08-18
*
|
|
|
Merge PR #972: 8.7 change entries
Maxime Dénès
2017-08-17
|
\
\
\
\
*
\
\
\
\
Merge PR #490: A possible fix for #5391 (command line tools do not accept tra...
Maxime Dénès
2017-08-17
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #974: Change section caption, improve some wording
Maxime Dénès
2017-08-17
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #976: Document anonymous universes (PR #544).
Maxime Dénès
2017-08-17
|
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
Use the wording suggested by Gaetan.
Théo Zimmermann
2017-08-17
|
|
|
|
*
|
|
|
Addition suggested by Pierre-Marie.
Théo Zimmermann
2017-08-17
|
|
|
|
|
*
|
|
Change 8.7~alpha to 8.7+alpha.
Maxime Dénès
2017-08-17
|
|
|
|
|
*
|
|
Make Travis generate OSX packages.
Maxime Dénès
2017-08-17
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
Document anonymous universes (PR #544).
Gaëtan Gilbert
2017-08-17
|
/
/
/
/
/
/
|
|
|
|
*
/
Adding documentation for Printing Focused option.
Pierre Courtieu
2017-08-17
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Additions following Hugo's suggestions.
Théo Zimmermann
2017-08-16
|
*
|
|
|
mention that tactic is the identity or gives error
Paul Steckler
2017-08-16
|
|
|
*
|
Improve wording.
Théo Zimmermann
2017-08-16
|
|
|
*
|
Mention tclINDEPENDENTL (#349) in dev/doc/changes.
Théo Zimmermann
2017-08-16
|
|
|
*
|
8.7 CHANGES
Théo Zimmermann
2017-08-16
|
*
|
|
|
change section caption, improve some wording
Paul Steckler
2017-08-16
|
/
/
/
/
|
|
*
/
Porting #856 (8.6.1 CHANGES entries) to master
Théo Zimmermann
2017-08-16
|
|
/
/
|
/
|
|
*
|
|
Merge PR #957: Set detachable windows type hint to dialog.
Maxime Dénès
2017-08-16
|
\
\
\
*
\
\
\
Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style
Maxime Dénès
2017-08-16
|
\
\
\
\
*
\
\
\
\
Merge PR #912: Detyping functions are now operating on EConstr.t.
Maxime Dénès
2017-08-16
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #942: solving b1859
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #954: Print names of all open blocks
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #964: More portable location for the time command.
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #951: Makefile: install-byte works even if -coqide no
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #944: Fix typos. Improve wording.
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #943: Reference Manual: minor wording improvements
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #940: Replace jarring use of "Remark" with "Note"
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #934: Fix some coq-tex errors in the reference manual.
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wr...
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #864: Some cleanups after cumulativity for inductive types
Maxime Dénès
2017-08-16
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
[next]