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
*
Minor debug printing bug,
Matthieu Sozeau
2016-11-16
*
Revert more of a477dc for good measure
Matthieu Sozeau
2016-11-16
*
Merge remote-tracking branch 'github/pr/358' into v8.6
Maxime Dénès
2016-11-15
|
\
|
*
Revert part of a477dc, disallow_shelved
Matthieu Sozeau
2016-11-15
|
/
*
Remove README.win until we come up with new instructions.
Maxime Dénès
2016-11-14
*
Set version number to 8.6beta1.
Maxime Dénès
2016-11-14
*
Remove the list of bug fixes from CHANGES.
Maxime Dénès
2016-11-14
*
Fix bug in warnings: -w foo was silent when foo did not exist.
Maxime Dénès
2016-11-14
*
Do not mention "none" in warnings doc, as it is there for compatibility.
Maxime Dénès
2016-11-14
*
Coqide: fixing default local links for refman and stdlib.
Hugo Herbelin
2016-11-11
*
Making explicit that a result is discarded (ocaml warning).
Hugo Herbelin
2016-11-11
*
Move OSX script.
Maxime Dénès
2016-11-10
*
Add Michael Soegtrop's new script to build windows installer.
Maxime Dénès
2016-11-10
*
Remove old windows build scripts.
Maxime Dénès
2016-11-10
*
Update CHANGES and credits for 8.6beta1.
Maxime Dénès
2016-11-10
*
Updating a comment in test-suite.
Hugo Herbelin
2016-11-10
*
Merge commit 'b385fbb' into v8.6
Maxime Dénès
2016-11-08
|
\
|
*
Use pf_get_type_of to avoid blowup in pose proof of large proof terms
Matthieu Sozeau
2016-11-08
*
|
Merge remote-tracking branch 'github/pr/348' into v8.6
Maxime Dénès
2016-11-08
|
\
\
*
|
|
Update documentation of Arguments after recent changes.
Maxime Dénès
2016-11-08
|
*
|
Rewording from Enrico
Matthieu Sozeau
2016-11-08
|
*
|
After Emilio's comment.
Matthieu Sozeau
2016-11-07
*
|
|
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
Mention notypeclasses refine in CHANGES
Matthieu Sozeau
2016-11-07
|
*
|
CHANGES for this branch.
Matthieu Sozeau
2016-11-07
|
*
|
Document two new variants of refine
Matthieu Sozeau
2016-11-07
|
*
|
Fixes to compile with ocaml 4.01
Matthieu Sozeau
2016-11-07
|
|
*
More accurate contributor list.
Matthieu Sozeau
2016-11-07
|
|
*
Hugo and Maxime's 2nd pass of comments
Matthieu Sozeau
2016-11-07
*
|
|
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
|
\
\
\
*
|
|
|
Improve formatting of a message in [Arguments].
Maxime Dénès
2016-11-07
*
|
|
|
Fix #5181: [Arguments] no longer correctly checks the length of arguments lists
Maxime Dénès
2016-11-07
*
|
|
|
Fix #5182: "Arguments names must be distinct." is bogus and underinformative
Maxime Dénès
2016-11-07
|
*
|
|
More explicit name for status of unification constraints.
Maxime Dénès
2016-11-07
|
|
|
*
Hugo's comments
Matthieu Sozeau
2016-11-06
|
|
|
*
Maxime's comments
Matthieu Sozeau
2016-11-06
|
|
|
*
Fixes from Enrico's review
Matthieu Sozeau
2016-11-06
*
|
|
|
Not using style tags when translating/beautifying a file.
Hugo Herbelin
2016-11-05
*
|
|
|
Removing a special treatment for empty lines in comments.
Hugo Herbelin
2016-11-05
*
|
|
|
Removing obsolete parsing of strings à la v7 in comments.
Hugo Herbelin
2016-11-05
|
|
|
*
Credits for 8.6
Matthieu Sozeau
2016-11-05
|
|
|
*
Minor fix in documentation
Matthieu Sozeau
2016-11-05
|
|
_
|
/
|
/
|
|
*
|
|
Do not print dependent evars by default (expensive)
Matthieu Sozeau
2016-11-05
*
|
|
More precise refine compatibility
Matthieu Sozeau
2016-11-05
*
|
|
Quick fix of tactic parsing while Load-ing in coqide.
Hugo Herbelin
2016-11-04
*
|
|
Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).
Hugo Herbelin
2016-11-04
*
|
|
Fix #3441 Use pf_get_type_of to avoid blowup
Matthieu Sozeau
2016-11-04
*
|
|
Fix refine in compatibility mode
Matthieu Sozeau
2016-11-04
*
|
|
Fix #4837: ./configure -local makes coqdep issue many warnings
Maxime Dénès
2016-11-04
*
|
|
Merge remote-tracking branch 'github/pr/335' into v8.6
Maxime Dénès
2016-11-04
|
\
\
\
[next]