aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness
Commit message (Expand)AuthorAge
* Suppression de la partie ML de la contrib correctness. Les fichiersGravatar herbelin2008-04-29
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* useless Require Export ExtractionGravatar letouzey2007-11-06
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Traduction des noms v7 en noms v8Gravatar herbelin2005-12-25
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* bugs avec Pose et AssertGravatar barras2004-01-09
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Parenthesage du terme pour accepter 'of' comme non identGravatar herbelin2003-12-24
* 'of' restait par erreur mot-cle dans psyntax.ml4 en v8Gravatar herbelin2003-12-23
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Remplacement de l'indicateur de date "@" par 'at'Gravatar herbelin2003-11-26
* Prise en compte des defs syntaxiques dans is_global et global_reference qui p...Gravatar herbelin2003-11-24
* Prise en compte renommagesGravatar herbelin2003-11-19
* Correction chemin de ZGravatar herbelin2003-11-14
* traduction des noms de correctnessGravatar herbelin2003-10-30
* Affichage des buts par Pfedit pour utilisation par les tactiquesGravatar herbelin2003-10-10
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Cacher les .v8Gravatar herbelin2003-10-03
* Changement de l'afficheur pour que les variables liées aient un nom indépen...Gravatar herbelin2003-09-23
* Indépendance vis à vis de DeclareGravatar herbelin2003-09-12
* Mise en place possibilité de définitions locales dans les paramètres des r...Gravatar herbelin2003-09-06
* Traducteur de correctnessGravatar herbelin2003-08-14
* code mortGravatar herbelin2003-08-14
* Notation access au dessous du niveau applicatif (2eme)Gravatar herbelin2003-08-14
* Notation access au dessous du niveau applicatifGravatar herbelin2003-08-13
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* DiversGravatar herbelin2003-04-17
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* * Ajout du traducteur nouvelle syntaxe *Gravatar barras2003-03-12
* Evaluation paresseuse de l'affichage du debugGravatar herbelin2002-12-15
* Compensation de suppression betaiota de type_ofGravatar herbelin2002-12-11
* Normalisation des types (fait avant dans Typing)Gravatar herbelin2002-12-10
* Court-circuit de g_zsyntaxGravatar herbelin2002-11-28
* Remplacement Grammar/Syntax par NotationGravatar herbelin2002-11-26
* typoGravatar herbelin2002-11-18