aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/psyntax.ml4
AgeCommit message (Expand)Author
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