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
*
CHANGES update
pboutill
2011-04-28
*
Coqide: try to properly send interrupts to coqtop on Win32
letouzey
2011-04-28
*
Updating CHANGES
herbelin
2011-04-27
*
Fixed a bug of destruct which was sometimes forgetting local definitions behi...
herbelin
2011-04-24
*
Add directories in COQPATH to search path.
herbelin
2011-04-14
*
Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395
pboutill
2011-04-08
*
Update documentation concerning proofs loading (cf last commit)
letouzey
2011-04-03
*
CHANGES: a word about recent changes in coqide, about Ctrl-C in vm
letouzey
2011-04-01
*
Documentation of the timeout tactical (cf r13917)
letouzey
2011-03-21
*
An option "Set Default Timeout n."
letouzey
2011-03-17
*
CHANGES: mentionning quickly Separate Extraction
letouzey
2011-03-07
*
CHANGES: update of syntax for annotations of functor application
letouzey
2011-03-04
*
Extraction: improved indentation of extracted code (fix #2497)
letouzey
2011-03-04
*
Update changelogs
glondu
2011-02-11
*
Fixpoints are traverse during implicits arguments search to toplevel
pboutill
2011-02-10
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Update CHANGES
pboutill
2011-01-07
*
First release of Vector library.
pboutill
2010-12-10
*
ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2
letouzey
2010-12-09
*
Numbers and bitwise functions.
letouzey
2010-12-06
*
Document new tactics in CHANGES
glondu
2010-12-02
*
CHANGES: mention some changes in trunk since the 8.3 fork
letouzey
2010-11-19
*
SearchAbout: who has never been annoyed by the [ ] syntax ?
letouzey
2010-11-19
*
CHANGES: small re-sync with the one of branch v8.3
letouzey
2010-11-19
*
Document DOT output of universe graph
glondu
2010-11-02
*
update CHANGES w.r.t. extraction
letouzey
2010-10-08
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Update CHANGES: Local/Global Set/Unset.
aspiwack
2010-09-23
*
Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +
herbelin
2010-09-02
*
Documentation of Set Automatic Coercions Import.
herbelin
2010-07-25
*
Made coercions active only when modules are imported.
herbelin
2010-07-22
*
Extraction Library Foo creates Foo.ml, not foo.ml
letouzey
2010-07-07
*
CHANGES: mention last-minute improvements of extraction
letouzey
2010-07-07
*
Remove dependency to Unix from module Profile
glondu
2010-07-02
*
Made "replace" accepts open terms on its left-hand-side.
herbelin
2010-06-28
*
Applying François' patches about Canonical Projections (see #2302 and #2334).
herbelin
2010-06-26
*
Commit 13179 continued (updated CHANGES about support for Heq's library).
herbelin
2010-06-22
*
Documentation of clear dependent and revert dependent
letouzey
2010-06-18
*
CHANGE: a word about new commands Compute and Fail
letouzey
2010-06-15
*
CHANGES: list of modifications for the extraction
letouzey
2010-06-15
*
Alert on the possible incompatibilties with set_add (see bug 2111) which
herbelin
2010-06-14
*
Keep description of Automatic Introduction at only one place of CHANGES.
herbelin
2010-06-09
*
Automatic introduction of names given before ":" in Lemma's and
herbelin
2010-06-09
*
Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.
herbelin
2010-06-09
*
Document grammar.cma->unix.cma dependency in CHANGES
glondu
2010-06-07
*
Added command "Locate Ltac qid".
herbelin
2010-06-03
*
plugin groebner updated and renamed as nsatz; first version of the doc of nsa...
pottier
2010-06-03
*
Missing warning flush in a lexer message + update of CHANGES
herbelin
2010-05-12
*
Applying François Garillot's patch (#2261 in bug tracker) for extended
herbelin
2010-04-22
[next]