| Commit message (Expand) | Author | Age |
* | 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 |
* | Code simplification in CC | corbinea | 2003-11-20 |
* | Prise en compte renommages | herbelin | 2003-11-19 |
* | correction suite ajout nouvelles tactiques | clrenard | 2003-11-18 |
* | Ajout Print Implicit avec depliage du type | herbelin | 2003-11-15 |
* | Ordre standard pour l'associativite | herbelin | 2003-11-14 |
* | Correction chemin de Z | herbelin | 2003-11-14 |
* | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras | 2003-11-13 |
* | factorisation et generalisation des clauses | barras | 2003-11-13 |
* | 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 | 2003-11-12 |
* | les modifs depuis la 7.4 | letouzey | 2003-11-12 |
* | TODO | letouzey | 2003-11-12 |
* | Extraction Module M devient simplement Extraction M | letouzey | 2003-11-12 |
* | Suppression SearchNamed finalement redondant avec SearchAbout | herbelin | 2003-11-10 |
* | le pb du <<.v vu comme module>> engendre maintenant une erreur | letouzey | 2003-11-10 |
* | message informant de l'ecriture d'un fichier extrait | letouzey | 2003-11-10 |