| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-06 | fixed groebner as a plugin + pattern matching Timeout | barras |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-05-21 | refined the conversion oracle | barras |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-08-22 | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest |
| 2006-05-02 | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-02-10 | induction now admits multiple induction arguments. The principle must | coq |
| 2005-05-20 | New command: "Print Ltac qualid" to print user defined tactics. | sacerdot |
| 2005-01-13 | Construct "T with (Definition|Module) id := c" generalized to | sacerdot |
| 2004-11-17 | New command "Print Rewrite HindDb dbname". | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-07-23 | "Show Setoids" command added. | sacerdot |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-03-03 | takes better account of the new possibility to pass a parametric count argument | bertot |
| 2004-02-19 | makes sure the following examples are well-treated: | bertot |
| 2004-02-18 | - fixed the Assert_failure error in kernel/modops | barras |
| 2004-02-16 | accomodate the .. extension | bertot |
| 2004-02-13 | adds the possibility to have terms (and not just identifiers) as hints | bertot |
| 2004-02-12 | Implicits can have an optional list of argument, which is different | bertot |
| 2004-02-02 | adds the possibility to mark function arguments as formulas in Ltac | bertot |
| 2004-01-30 | updates the definition of tactics using Ltac and adds the subst tactic | bertot |
| 2004-01-29 | updates the tactics contradiction and autorewrite, the commands | bertot |
| 2004-01-28 | make sure that 'in' clauses for reduction tactics are translated | bertot |
| 2004-01-26 | a try to make intro patterns better | bertot |
| 2004-01-24 | streamlines the keywords for definitions, require commandsbinders, notation | bertot |
| 2004-01-22 | change add path commands to get the extra argument and the Hint commands | bertot |
| 2004-01-22 | fixes argument lists for tactic definitions, updates inversion tactics | bertot |
| 2004-01-22 | adds a clause argument to symmetry | bertot |
| 2004-01-22 | adds the notations in inductive definitions, improves the consistency between | bertot |
| 2004-01-22 | handles explicit function calls, names meta variables in patterns | bertot |
| 2004-01-21 | updates the structure of fix (struct argument added) and if | bertot |
| 2004-01-19 | 1.20 | bertot |
| 2004-01-19 | adds constructs to handle notations in patterns | bertot |
| 2004-01-15 | translation to structures now okay for pattern matching constructs | bertot |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-16 | nouvelle syntaxe de ltac | barras |
| 2003-01-26 | all tactics should be covered now: remains | bertot |
| 2003-01-25 | Add translations for many tactics but a dozen are still remaining | bertot |
| 2003-01-22 | removes all references to ctast.ml the Makefile has been updated accordingly. | bertot |
| 2003-01-21 | Add a few operators in the new version of xlate.ml and make sure | bertot |
| 2002-12-09 | Ajoute le bon traitement pour Ring, Locate, Comments | bertot |
| 2002-12-09 | Take notations into account: numbers and the CNotation operator. | bertot |
| 2002-12-03 | Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles | bertot |
| 2002-10-06 | correcting the treatment of many tactics that use quant_hyp in file xlate.ml | bertot |
