aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-26Remplacement de l'indicateur de date "@" par 'at'herbelin
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-19Prise en compte renommagesherbelin
2003-11-14Correction chemin de Zherbelin
2003-10-30traduction des noms de correctnessherbelin
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiquesherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-03Cacher les .v8herbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-12Indépendance vis à vis de Declareherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-08-14Traducteur de correctnessherbelin
2003-08-14code mortherbelin
2003-08-14Notation access au dessous du niveau applicatif (2eme)herbelin
2003-08-13Notation access au dessous du niveau applicatifherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-17Diversherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-12* Ajout du traducteur nouvelle syntaxe *barras
2002-12-15Evaluation paresseuse de l'affichage du debugherbelin
2002-12-11Compensation de suppression betaiota de type_ofherbelin
2002-12-10Normalisation des types (fait avant dans Typing)herbelin
2002-11-28Court-circuit de g_zsyntaxherbelin
2002-11-26Remplacement Grammar/Syntax par Notationherbelin
2002-11-18typoherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-09-19portage Correctness (substitutivité pour les modules)filliatr
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19ProgWf -> Zwffilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-06-03Factorisation de 'Show Programs' au premier niveau de Vernac_.commandherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2002-02-08affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 16:08:19 +0000