aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/putil.ml
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...Gravatar filliatr2002-02-08
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* deux fichiers (past et ptype) uniquement sous forme de .mliGravatar filliatr2001-04-04
* mise en place de Correctness (ne compile pas encore)Gravatar filliatr2001-03-29