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
*
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
*
A pass on the CHANGES file + credits for 8.3 (completing commit 12906
herbelin
2010-04-17
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)
herbelin
2010-03-28
*
Updated CHANGES wrt 8.3
herbelin
2010-03-23
*
Added automatic expansion on the left of recursive notations
herbelin
2010-03-23
*
update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 r...
letouzey
2010-02-14
*
Documentation of the ! annotation for functor application
letouzey
2010-02-11
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
Update CHANGES, add documentation for new commands/tactics and do a bit
msozeau
2010-01-30
*
New command Declare Reduction <id> := <conv_expr>.
letouzey
2010-01-28
*
Document Local Declare ML Module
glondu
2010-01-14
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
Specific syntax for Instances in Module Type: Declare Instance
letouzey
2010-01-04
*
Few misc. updates.
herbelin
2010-01-04
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Description of the new features of the module system (part two).
soubiran
2009-12-15
*
Description of the new features of the module system (first part).
soubiran
2009-12-15
*
Improved strategy for rewriting lemma possibly depending because of evars.
herbelin
2009-12-14
*
Addition of mergesort + cleaning of the Sorting library
herbelin
2009-12-13
*
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
2009-12-13
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)
herbelin
2009-12-03
*
Continuing r12485-12486 and r12549 (cleaning around name generation)
herbelin
2009-12-02
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Experiment propagation of implicit arguments and arguments scope for
herbelin
2009-11-12
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
Improving abbreviations/notations + backtrack of semantic change in r12439
herbelin
2009-11-11
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Made that notations to names behave like the names they refer to wrt
herbelin
2009-10-28
[next]