index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
CHANGES
Commit message (
Expand
)
Author
Age
*
A few words in CHANGES.
Maxime Dénès
2016-12-07
*
Fix some documentation typos.
Guillaume Melquiond
2016-11-24
*
[doc] Mention XML protocol on changes.
Emilio Jesus Gallego Arias
2016-11-16
*
Remove the list of bug fixes from CHANGES.
Maxime Dénès
2016-11-14
*
Update CHANGES and credits for 8.6beta1.
Maxime Dénès
2016-11-10
*
Mention notypeclasses refine in CHANGES
Matthieu Sozeau
2016-11-07
*
CHANGES for this branch.
Matthieu Sozeau
2016-11-07
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
\
|
*
Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."
Maxime Dénès
2016-10-25
|
*
Update CHANGES.
Maxime Dénès
2016-10-25
*
|
Tentatively preparing to add changes specific to v8.7 (see PR #275).
Hugo Herbelin
2016-10-12
*
|
Report about changes of semantics of auto as an ltac argument (see #4966).
Hugo Herbelin
2016-10-08
*
|
Remove the Set Verbose Compat option and turn the warning on by default.
Maxime Dénès
2016-10-06
*
|
Document change related to Keep Proof Equalities in CHANGES.
Maxime Dénès
2016-10-03
*
|
Being more informative about the change of behavior of "subst".
Hugo Herbelin
2016-09-29
*
|
Fix description of change in intro semantics.
Maxime Dénès
2016-09-21
*
|
Extending "contradiction" so that it recognizes statements such as "~x=x" or ...
Hugo Herbelin
2016-09-15
*
|
Refolding: disable in 8.4 compat file, document
Matthieu Sozeau
2016-09-12
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-08-21
|
\
|
|
*
Fixing CHANGES.
Hugo Herbelin
2016-08-17
*
|
Documenting fix of #3070 (subst and chain of dependencies).
Hugo Herbelin
2016-08-17
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-08-16
|
\
|
|
*
Fix #5000: Document the native compiler soundness bug due to Unicode mangling.
Pierre-Marie Pédrot
2016-08-07
|
*
Fix bug #4673: regression in setoid_rewrite.
Matthieu Sozeau
2016-07-29
*
|
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-29
|
\
|
|
*
Update CHANGES about #3886 bugfix
Matthieu Sozeau
2016-07-29
|
*
Fix #4769, univ poly and elim schemes in sections
Matthieu Sozeau
2016-07-29
|
*
Update CHANGES about critical bugfix and others
Matthieu Sozeau
2016-07-26
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-20
|
\
|
|
*
Update CHANGES
Matthieu Sozeau
2016-07-20
*
|
Update CHANGES
Matthieu Sozeau
2016-07-20
*
|
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-18
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-13
|
\
|
|
*
Add a few fixes in CHANGES that were forgotten.
Maxime Dénès
2016-07-08
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
|
*
congruence fix: test-suite code and update CHANGES
Matthieu Sozeau
2016-07-05
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
|
\
|
*
|
Update CHANGES, the bugfixes for 4527 and 4726 are
Matthieu Sozeau
2016-07-04
|
*
Mention more fixes in CHANGES before we release pl2.
Maxime Dénès
2016-07-04
*
|
Updated CHANGES about subst. More on recursive equations in reference manual.
Hugo Herbelin
2016-06-29
*
|
CHANGES: document fix for #4726 too.
Matthieu Sozeau
2016-06-29
*
|
CHANGES: document fix for 4527 and compatibility.
Matthieu Sozeau
2016-06-29
*
|
Merge remote-tracking branch 'github/pr/207' into trunk
Maxime Dénès
2016-06-28
|
\
\
|
|
*
Univs/CHANGES: #4097 and annotations on notations
Matthieu Sozeau
2016-06-27
*
|
|
Update CHANGES and COMPATIBILITY
Matthieu Sozeau
2016-06-27
*
|
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
|
*
|
Add [Unset Printing Dependent Evars Line]
Jason Gross
2016-06-19
|
/
/
*
|
Giving a more natural semantics to injection by default.
Hugo Herbelin
2016-06-18
*
|
Mentioning goal selectors in CHANGES
Enrico Tassi
2016-06-17
*
|
Fix wrong tabulation in CHANGES
Matthieu Sozeau
2016-06-16
[next]