aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/ptactic.ml
Commit message (Expand)AuthorAge
* 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