aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2009-12-15Description of the new features of the module system (first part).soubiran
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-12Experiment propagation of implicit arguments and arguments scope forherbelin
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
2009-10-27Added option --external to coqdoc to bind an url to an external library.herbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-08Fixed clash names in Relations (see bug report #2152) and make namesherbelin
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:36:41 +0000