| Age | Commit message (Expand) | Author |
|---|
| 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-30 | adds module commands and update the extration command | bertot |
| 2004-01-29 | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin |
| 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 | corrects the way the structural argument declaration is handled in | 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 | handles projector notations, cases with return types, | 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-14 | compact nested universal quantifications into a single quantification with | bertot |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-25 | Uniformisation des politiques de nommage de NewDestruct sur arguments recursi... | herbelin |
| 2003-11-18 | correction suite ajout nouvelles tactiques | clrenard |
| 2003-11-15 | Ajout Print Implicit avec depliage du type | herbelin |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-11-12 | Bug TacId | herbelin |
| 2003-11-10 | Suppression SearchNamed finalement redondant avec SearchAbout | herbelin |
| 2003-11-09 | Traduction semantique des InHyp de clause en InHypValue si local def | herbelin |
| 2003-11-06 | Added Instantiate ... in | corbinea |
| 2003-11-01 | Ajout CPatNotation, PrintVisibility | herbelin |
| 2003-10-23 | Conjecture declare maintenant un axiome; reorganisation VernacDefinition | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-16 | nouvelle syntaxe de ltac | barras |
| 2003-10-13 | Ajout d'une fonction de recherche sur les composantes du nom des objets | herbelin |
| 2003-10-10 | Cablage en dur de inversion | herbelin |
| 2003-10-10 | changement nouvelle syntaxe (pt fixes) | barras |
| 2003-10-08 | Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in... | herbelin |
| 2003-09-30 | Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format' | herbelin |
| 2003-09-23 | Utilisation de noms dans 'Implicit Arguments [...]' | herbelin |
| 2003-09-21 | Mise en place d'implicites par noms en v8 | herbelin |
| 2003-09-19 | parsing | herbelin |
| 2003-09-12 | Ajout 'Print Scopes' et 'Bind Scope with classes' | herbelin |
| 2003-09-09 | Ajout construction If primitive dans constr_expr et rawconstr | herbelin |
| 2003-09-06 | Mise en place possibilité de définitions locales dans les paramètres des r... | herbelin |
| 2003-09-06 | Mise en place possibilité de définitions locales dans les paramètres des i... | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-06-19 | Ajout 'Symmetry in Hyp' | herbelin |
