aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness
AgeCommit message (Collapse)Author
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Traduction des noms v7 en noms v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7728 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09bugs avec Pose et Assertbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24Parenthesage du terme pour accepter 'of' comme non identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5148 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23'of' restait par erreur mot-cle dans psyntax.ml4 en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Remplacement de l'indicateur de date "@" par 'at'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4998 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵herbelin
passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Prise en compte renommagesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4950 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Correction chemin de Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4904 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30traduction des noms de correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4743 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4563 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom ↵herbelin
indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Indépendance vis à vis de Declareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4379 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Traducteur de correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4275 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4274 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Notation access au dessous du niveau applicatif (2eme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4267 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-13Notation access au dessous du niveau applicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4265 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4055 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12* Ajout du traducteur nouvelle syntaxe *barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3760 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Evaluation paresseuse de l'affichage du debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3435 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-11Compensation de suppression betaiota de type_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3421 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Normalisation des types (fait avant dans Typing)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3414 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Court-circuit de g_zsyntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3329 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Remplacement Grammar/Syntax par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3305 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3255 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-19portage Correctness (substitutivité pour les modules)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3019 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:20:45 +0000