aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/ptactic.ml
Commit message (Expand)AuthorAge
* Suppression de la partie ML de la contrib correctness. Les fichiersGravatar herbelin2008-04-29
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* Correction chemin de ZGravatar herbelin2003-11-14
* Affichage des buts par Pfedit pour utilisation par les tactiquesGravatar herbelin2003-10-10
* code mortGravatar herbelin2003-08-14
* 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
* * Ajout du traducteur nouvelle syntaxe *Gravatar barras2003-03-12
* Evaluation paresseuse de l'affichage du debugGravatar herbelin2002-12-15
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* retablissement de Correctness (pas encore teste' cependant)Gravatar filliatr2002-09-18
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* ProgWf -> ZwfGravatar filliatr2002-06-19
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
* affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...Gravatar filliatr2002-02-08
* le save de Correctness faisant assert falseGravatar barras2001-12-17
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* nettoyageGravatar filliatr2001-05-28
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Modification afin de permettre plusieurs modifs successives d'une commandeGravatar clrenard2001-05-18
* expansion des constr pursGravatar filliatr2001-04-23
* remplace Zarith par ZArithGravatar mohring2001-04-19
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* mise en place de Correctness (ne compile pas encore)Gravatar filliatr2001-03-29