aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/psyntax.ml4
AgeCommit message (Expand)Author
2003-11-26Remplacement de l'indicateur de date "@" par 'at'herbelin
2003-11-19Prise en compte renommagesherbelin
2003-10-30traduction des noms de correctnessherbelin
2003-08-14Traducteur de correctnessherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2002-11-28Court-circuit de g_zsyntaxherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-06-03Factorisation de 'Show Programs' au premier niveau de Vernac_.commandherbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-02-21code mort dans tactinterp; plus de Debug On/Off dans Correctnessfilliatr
2002-01-21Zinv -> Zoppfilliatr
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
2001-11-05GROS COMMIT:barras
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-08-10Parsingherbelin
2001-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
2001-05-28nettoyagefilliatr
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
2001-04-03psyntax.ml4 sous CVSfilliatr