aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Made coercions active only when modules are imported.Gravatar herbelin2010-07-22
* Extraction Library Foo creates Foo.ml, not foo.mlGravatar letouzey2010-07-07
* CHANGES: mention last-minute improvements of extractionGravatar letouzey2010-07-07
* Remove dependency to Unix from module ProfileGravatar glondu2010-07-02
* Made "replace" accepts open terms on its left-hand-side.Gravatar herbelin2010-06-28
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* Commit 13179 continued (updated CHANGES about support for Heq's library).Gravatar herbelin2010-06-22
* Documentation of clear dependent and revert dependentGravatar letouzey2010-06-18
* CHANGE: a word about new commands Compute and FailGravatar letouzey2010-06-15
* CHANGES: list of modifications for the extractionGravatar letouzey2010-06-15
* Alert on the possible incompatibilties with set_add (see bug 2111) whichGravatar herbelin2010-06-14
* Keep description of Automatic Introduction at only one place of CHANGES.Gravatar herbelin2010-06-09
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Document grammar.cma->unix.cma dependency in CHANGESGravatar glondu2010-06-07
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* plugin groebner updated and renamed as nsatz; first version of the doc of nsa...Gravatar pottier2010-06-03
* Missing warning flush in a lexer message + update of CHANGESGravatar herbelin2010-05-12
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
* A pass on the CHANGES file + credits for 8.3 (completing commit 12906Gravatar herbelin2010-04-17
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)Gravatar herbelin2010-03-28
* Updated CHANGES wrt 8.3Gravatar herbelin2010-03-23
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 r...Gravatar letouzey2010-02-14
* Documentation of the ! annotation for functor applicationGravatar letouzey2010-02-11
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Document Local Declare ML ModuleGravatar glondu2010-01-14
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Few misc. updates.Gravatar herbelin2010-01-04
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Description of the new features of the module system (part two).Gravatar soubiran2009-12-15
* Description of the new features of the module system (first part).Gravatar soubiran2009-12-15
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)Gravatar herbelin2009-12-03
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 20:34:02 +0000