aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/psyntax.ml4
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-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2006-04-27Standardisation nom option_app en option_mapherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-25Traduction des noms v7 en noms v8herbelin
2004-07-16Nouvelle en-têteherbelin
2003-12-24Parenthesage du terme pour accepter 'of' comme non identherbelin
2003-12-23'of' restait par erreur mot-cle dans psyntax.ml4 en v8herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:35 +0000