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
*
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
*
|
Fix after merge, the revert of Bind Scope applies to trunk only.
Matthieu Sozeau
2016-04-04
*
|
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
\
*
|
|
All arguments defined through ARGUMENT EXTEND declare a tactic scope.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
|
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
*
|
|
Fixing some problems with double induction.
Hugo Herbelin
2016-01-21
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Reporting about the new tactical unshelve.
Hugo Herbelin
2016-01-12
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
|
|
|
*
|
Update version numbers and magic numbers for 8.5rc1 release.
Maxime Dénès
2015-12-16
|
*
|
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Guillaume Melquiond
2015-12-16
|
*
|
Proof using: do not clear unused section hyps automatically
Enrico Tassi
2015-12-15
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-15
|
\
|
|
|
*
|
Updating CHANGES with an incompatibility.
Hugo Herbelin
2015-12-14
|
*
|
Flag -compat 8.4 now loads Coq.Compat.Coq84.
Maxime Dénès
2015-12-14
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
|
*
|
Document removal of Set Virtual Machine and -vm in CHANGES.
Maxime Dénès
2015-12-11
|
*
|
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
*
|
Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)
Hugo Herbelin
2015-12-05
|
*
|
Fix CHANGES.
Hugo Herbelin
2015-12-05
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
|
*
|
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Hugo Herbelin
2015-12-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
|
*
|
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
|
*
|
Update CHANGES
Jason Gross
2015-11-12
|
*
|
Fix bug #3735: interpretation of "->" in Program follows the standard one.
Matthieu Sozeau
2015-11-11
*
|
|
Listing separately changes from 8.5betas to final 8.5 and further
Hugo Herbelin
2015-11-10
*
|
|
Activating bracketing of last or-and introduction pattern by default
Hugo Herbelin
2015-11-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
|
*
|
Update version numbers and magic numbers for 8.5beta3 release.
Maxime Dénès
2015-11-05
|
*
|
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
|
*
|
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
|
*
|
Mention bug 3199 fix as a source of incompatibilities.
Matthieu Sozeau
2015-10-21
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
|
|
*
|
Documenting the option "Strict Universe Declaration" in CHANGES.
Pierre-Marie Pédrot
2015-10-19
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
|
*
|
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
|
*
|
Remove the "exists" overrides from Program. (Fix bug #4360)
Guillaume Melquiond
2015-10-07
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
[next]