| Commit message (Expand) | Author | Age |
* | New version of Functional Scheme and functional induction. Deals with | coq | 2004-02-09 |
* | correction de bugs de congruence et firstorder (inductifs) | corbinea | 2004-02-06 |
* | adds the possibility to mark function arguments as formulas in Ltac | bertot | 2004-02-02 |
* | 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 |
* | adds module commands and update the extration command | bertot | 2004-01-30 |
* | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin | 2004-01-29 |
* | 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 |
* | 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-22 |
* | updates the structure of fix (struct argument added) and if | bertot | 2004-01-21 |
* | 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-19 |
* | translation to structures now okay for pattern matching constructs | bertot | 2004-01-15 |
* | 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-14 |
* | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin | 2004-01-13 |
* | bugs avec Pose et Assert | barras | 2004-01-09 |
* | meilleure presentation des commentaires du traducteur | barras | 2004-01-02 |
* | 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-24 |
* | '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-23 |
* | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras | 2003-12-15 |
* | cc update | corbinea | 2003-12-09 |
* | error messages adjustement | corbinea | 2003-12-02 |
* | Nouvelle tactique EExists | clrenard | 2003-12-01 |
* | 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-29 |
* | Retour des _eq en v8 | herbelin | 2003-11-27 |
* | 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-26 |
* | Uniformisation des politiques de nommage de NewDestruct sur arguments recursi... | herbelin | 2003-11-25 |
* | CC: added injection theory | corbinea | 2003-11-25 |
* | Prise en compte des defs syntaxiques dans is_global et global_reference qui p... | herbelin | 2003-11-24 |