| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 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-10 | 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 | révision du traitement des axiomes non réalisés | letouzey |
| 2003-11-10 | essai d'extraction sous un module | letouzey |
| 2003-11-09 | factorisation de (recursive) library | letouzey |
| 2003-11-09 | Traduction semantique des InHyp de clause en InHypValue si local def | 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-05 | Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif... | herbelin |
| 2003-11-05 | Renommage canonique d'un lemme redondant | herbelin |
| 2003-11-05 | Déport des lemmes de Omega de ZArith vers OmegaLemmas | herbelin |
| 2003-11-05 | Renommage canonique d'un lemme redondant | herbelin |
| 2003-11-04 | Extension de zarith | herbelin |
| 2003-11-02 | Protection contre les buts sans inegalite | herbelin |
| 2003-11-01 | Ajout CPatNotation, PrintVisibility | herbelin |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-30 | Redirected some of the verbose jprover output through the Pp module. | corbinea |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
