| Age | Commit message (Expand) | Author |
|---|
| 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 | 1.20 | bertot |
| 2004-01-19 | 1.19 | 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-14 | make sure the parser for FORMULA does not require them to be enclosed in | bertot |
| 2004-01-14 | Now, the grammar extension from .v files are concentrated in just a few | 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-24 | Parenthesage du terme pour accepter 'of' comme non ident | herbelin |
| 2003-12-24 | La correction precedente a mis en evidence un defaut de l'utilisation de intr... | herbelin |
| 2003-12-23 | 'of' restait par erreur mot-cle dans psyntax.ml4 en v8 | herbelin |
| 2003-12-23 | Retablissement de GIntuition juste pour FSets | herbelin |
| 2003-12-23 | *** empty log message *** | barras |
| 2003-12-23 | Renommages des hypotheses transformees car en raison des possibles dependance... | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-09 | cc update | corbinea |
| 2003-12-02 | error messages adjustement | corbinea |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-29 | Obsolete, cf Funind.v dans test-suite | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-29 | ground->firstorder, cc-> congruence, CC final commit | corbinea |
| 2003-11-27 | Retour des _eq en v8 | herbelin |
| 2003-11-26 | Remplacement de l'indicateur de date "@" par 'at' | herbelin |
| 2003-11-26 | just forgot something in previous commit | corbinea |
| 2003-11-26 | removal of CC.v lemata in cc (deprecated) | corbinea |
| 2003-11-25 | Uniformisation des politiques de nommage de NewDestruct sur arguments recursi... | herbelin |
| 2003-11-25 | CC: added injection theory | corbinea |
| 2003-11-24 | Prise en compte des defs syntaxiques dans is_global et global_reference qui p... | herbelin |
| 2003-11-20 | Code simplification in CC | corbinea |
| 2003-11-19 | Prise en compte renommages | herbelin |
| 2003-11-18 | correction suite ajout nouvelles tactiques | clrenard |
| 2003-11-15 | Ajout Print Implicit avec depliage du type | herbelin |
| 2003-11-14 | Ordre standard pour l'associativite | herbelin |
| 2003-11-14 | Correction chemin de Z | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-11-12 | Bug TacId | herbelin |
| 2003-11-12 | Restructuration ZArith | herbelin |
| 2003-11-12 | Noms/énoncés plus canoniques | herbelin |
| 2003-11-12 | petits changements de syntaxe | barras |
