| Commit message (Expand) | Author | Age |
|---|
| * | New command: "Print Ltac qualid" to print user defined tactics. |  sacerdot | 2005-05-20 |
| * | Construct "T with (Definition|Module) id := c" generalized to | sacerdot | 2005-01-13 |
| * | New command "Print Rewrite HindDb dbname". | sacerdot | 2004-11-17 |
| * | COMMITED BYTECODE COMPILER |  barras | 2004-10-20 |
| * | "Show Setoids" command added. | sacerdot | 2004-07-23 |
| * | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras | 2004-03-05 |
| * | takes better account of the new possibility to pass a parametric count argument |  bertot | 2004-03-03 |
| * | makes sure the following examples are well-treated: | bertot | 2004-02-19 |
| * | - fixed the Assert_failure error in kernel/modops | barras | 2004-02-18 |
| * | accomodate the .. extension | bertot | 2004-02-16 |
| * | adds the possibility to have terms (and not just identifiers) as hints | bertot | 2004-02-13 |
| * | Implicits can have an optional list of argument, which is different | bertot | 2004-02-12 |
| * | adds the possibility to mark function arguments as formulas in Ltac | bertot | 2004-02-02 |
| * | updates the definition of tactics using Ltac and adds the subst tactic | bertot | 2004-01-30 |
| * | updates the tactics contradiction and autorewrite, the commands | bertot | 2004-01-29 |
| * | make sure that 'in' clauses for reduction tactics are translated | bertot | 2004-01-28 |
| * | a try to make intro patterns better | bertot | 2004-01-26 |
| * | streamlines the keywords for definitions, require commandsbinders, notation | bertot | 2004-01-24 |
| * | 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-22 |
| * | updates the structure of fix (struct argument added) and if | bertot | 2004-01-21 |
| * | 1.19 | bertot | 2004-01-19 |
| * | adds constructs to handle notations in patterns | bertot | 2004-01-19 |
| * | translation to structures now okay for pattern matching constructs | bertot | 2004-01-15 |
| * | bugs avec Pose et Assert | barras | 2004-01-09 |
| * | factorisation et generalisation des clauses | barras | 2003-11-13 |
| * | reorganisation des niveaux (ex: = est a 70) | barras | 2003-10-22 |
| * | nouvelle syntaxe de ltac | barras | 2003-10-16 |
| * | all tactics should be covered now: remains | bertot | 2003-01-26 |
| * | Add translations for many tactics but a dozen are still remaining | bertot | 2003-01-25 |
| * | removes all references to ctast.ml the Makefile has been updated accordingly. | bertot | 2003-01-22 |
| * | Add a few operators in the new version of xlate.ml and make sure | bertot | 2003-01-21 |
| * | Ajoute le bon traitement pour Ring, Locate, Comments | bertot | 2002-12-09 |
| * | Take notations into account: numbers and the CNotation operator. | bertot | 2002-12-09 |
| * | Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles | bertot | 2002-12-03 |
| * | correcting the treatment of many tactics that use quant_hyp in file xlate.ml | bertot | 2002-10-06 |
| * | Previous version did compile but did not make it possible to actually run | bertot | 2002-10-03 |
| * | Integrating the Ltac language and the Blast tool into the interface | bertot | 2001-12-18 |
| * | GROS COMMIT: | barras | 2001-11-05 |
| * | Adding files for the production of textual explanations as used in pcoq. | bertot | 2001-04-18 |
| * | Files that handle the dialogue with the graphical user-interface pcoq. | bertot | 2001-04-04 |
sacerdot
barras
bertot