aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/ptactic.ml
AgeCommit message (Expand)Author
2008-04-29Suppression de la partie ML de la contrib correctness. Les fichiersherbelin
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-14Correction chemin de Zherbelin
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiquesherbelin
2003-08-14code mortherbelin
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-03-12* Ajout du traducteur nouvelle syntaxe *barras
2002-12-15Evaluation paresseuse de l'affichage du debugherbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-19ProgWf -> Zwffilliatr
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-02-08affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...filliatr
2001-12-17le save de Correctness faisant assert falsebarras
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-05-28nettoyagefilliatr
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-18Modification afin de permettre plusieurs modifs successives d'une commandeclrenard
2001-04-23expansion des constr pursfilliatr
2001-04-19remplace Zarith par ZArithmohring
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-09branchement extraction en standard (pas de Require)filliatr
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...filliatr
2001-03-30branchement extraction (bytecode seulement)filliatr
2001-03-29mise en place de Correctness (ne compile pas encore)filliatr