aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-07Update CHANGESpboutill
2010-12-10First release of Vector library.pboutill
2010-12-09ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2letouzey
2010-12-06Numbers and bitwise functions.letouzey
2010-12-02Document new tactics in CHANGESglondu
2010-11-19CHANGES: mention some changes in trunk since the 8.3 forkletouzey
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
2010-11-19CHANGES: small re-sync with the one of branch v8.3letouzey
2010-11-02Document DOT output of universe graphglondu
2010-10-08update CHANGES w.r.t. extractionletouzey
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-09-23Update CHANGES: Local/Global Set/Unset.aspiwack
2010-09-02Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +herbelin
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
2010-07-22Made coercions active only when modules are imported.herbelin
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07CHANGES: mention last-minute improvements of extractionletouzey
2010-07-02Remove dependency to Unix from module Profileglondu
2010-06-28Made "replace" accepts open terms on its left-hand-side.herbelin
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-22Commit 13179 continued (updated CHANGES about support for Heq's library).herbelin
2010-06-18Documentation of clear dependent and revert dependentletouzey
2010-06-15CHANGE: a word about new commands Compute and Failletouzey
2010-06-15CHANGES: list of modifications for the extractionletouzey
2010-06-14Alert on the possible incompatibilties with set_add (see bug 2111) whichherbelin
2010-06-09Keep description of Automatic Introduction at only one place of CHANGES.herbelin
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-07Document grammar.cma->unix.cma dependency in CHANGESglondu
2010-06-03Added command "Locate Ltac qid".herbelin
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-05-12Missing warning flush in a lexer message + update of CHANGESherbelin
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-04-17A pass on the CHANGES file + credits for 8.3 (completing commit 12906herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-28Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)herbelin
2010-03-23Updated CHANGES wrt 8.3herbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-02-14update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 r...letouzey
2010-02-11Documentation of the ! annotation for functor applicationletouzey
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2010-01-14Document Local Declare ML Moduleglondu
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2010-01-04Few misc. updates.herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-15Description of the new features of the module system (part two).soubiran
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:11:00 +0000