aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness
Commit message (Expand)AuthorAge
* message 'is defined' seulement en mode verboseGravatar filliatr2001-05-10
* expansion des constr pursGravatar filliatr2001-04-23
* nettoyageGravatar filliatr2001-04-20
* remplace Zarith par ZArithGravatar mohring2001-04-19
* documentation automatique de la bibliothèque standardGravatar filliatr2001-04-11
* réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...Gravatar filliatr2001-04-11
* portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegaGravatar filliatr2001-04-10
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* exemples CorrectnessGravatar filliatr2001-04-09
* 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
* deux fichiers (past et ptype) uniquement sous forme de .mliGravatar filliatr2001-04-04
* psyntax.ml4 sous CVSGravatar filliatr2001-04-03
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* mise en place de Correctness (ne compile pas encore)Gravatar filliatr2001-03-29