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
*
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
*
|
Document new Hint Mode option.
Matthieu Sozeau
2016-06-16
*
|
Revise syntax of Hint Cut
Matthieu Sozeau
2016-06-16
*
|
Not taking arguments given by name or position into account when
Hugo Herbelin
2016-06-16
*
|
Merge PR #195: Complete is_* family of term-examining tactics.
Pierre-Marie Pédrot
2016-06-16
|
\
\
*
|
|
--print-version produces machine readable version info
Enrico Tassi
2016-06-16
|
*
|
Update CHANGES
Jason Gross
2016-06-16
*
|
|
Merge remote-tracking branch 'origin/pr/166' into trunk
Enrico Tassi
2016-06-14
|
\
\
\
*
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-13
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
/
|
|
|
/
|
|
/
|
|
*
|
Reporting about a few bug fixes (to be continued).
Hugo Herbelin
2016-06-09
*
|
|
Removing "intro" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
|
|
/
|
/
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
In Regular Subst Tactic mode, ensure that the order of hypotheses is
Hugo Herbelin
2016-05-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
|
|
*
Mention problems with fix of #4582 in CHANGES.
Maxime Dénès
2016-04-22
|
*
Mention #4548 (fixed) in CHANGES.
Maxime Dénès
2016-04-22
|
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
|
*
Add changelog for 8.5pl1 after the fact.
Maxime Dénès
2016-04-17
[next]