aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2011-06-10Updated CHANGES (info, Show Script, rephrasing).herbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-04-28CHANGES updatepboutill
2011-04-28Coqide: try to properly send interrupts to coqtop on Win32letouzey
2011-04-27Updating CHANGESherbelin
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions behi...herbelin
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-08Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395pboutill
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
2011-04-01CHANGES: a word about recent changes in coqide, about Ctrl-C in vmletouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-17An option "Set Default Timeout n."letouzey
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
2011-03-04CHANGES: update of syntax for annotations of functor applicationletouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-02-11Update changelogsglondu
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 00:23:52 +0000