coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	PolyList -> List	letouzey	2004-03-22
*	petit rajeunissement du test d'extraction	letouzey	2004-03-20
*	renommage des modules 1er niveau en monolithique	letouzey	2003-07-10
*	BIG MAJ Extraction:	letouzey	2003-04-16
*	Extraction des modules, enfin !	letouzey	2003-01-22
*	bug pp letin + un inductif constant n'est pas un record	letouzey	2002-11-28
*	maj avec tous les mli	letouzey	2002-11-04
*	Un fichier a utiliser via Drop pour le debug de l'extraction.	letouzey	2002-11-04
*	L'extraction c'est magic cvs -n up	letouzey	2002-10-31
*	maj	letouzey	2002-07-16
*	maj test des reals	letouzey	2002-04-12
*	ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...	letouzey	2002-04-08
*	mise jour	filliatr	2002-04-05
*	Refonte complete de la génération des types ML	letouzey	2002-03-26
*	reparation du test des reals	letouzey	2002-03-21
*	deux fichiers supplementaires de customisation d'extraction	letouzey	2002-03-21
*	changement du test extraction suite aux modif inining	letouzey	2002-03-21
*	Big commit extraction:	letouzey	2002-03-04
*	suite et fin (?) de haskell: gestion des modules, mise en place du'un test	letouzey	2002-02-15
*	qq inline manuels (sigS_rec ...) + utilisation de library_part	letouzey	2002-02-14
*	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey	2002-02-06
*	adaptation de l'extraction aux changements de Christine concernant rec/rect e...	letouzey	2002-01-31
*	debranchement du test sur les Reals	letouzey	2001-12-19
*	correction de bugs concernant la gestion des modules. debranchement du test d...	letouzey	2001-12-10
*	remise au gout du jour du repertoire theories/Sorting de la V6.3	letouzey	2001-11-21
*	Moins de fichiers avec des axioms	letouzey	2001-11-13
*	Refonte du fichier mlutil.ml. Correction d'un bug d'optim case	letouzey	2001-11-07
*	suite des tests	letouzey	2001-11-06
*	refonte du test	letouzey	2001-11-05
*	changement epsilonesque	letouzey	2001-11-03
*	retablissement de l'optim case constant	letouzey	2001-11-03
*	ajout du script qualify2open qui met des open Truc en debut de fichier	letouzey	2001-11-03
*	Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...	letouzey	2001-10-26
*	chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...	letouzey	2001-10-22
*	changements mineurs du test	letouzey	2001-09-20
*	adaptation a la nouvelle syntaxe Extract Inlined Constant	letouzey	2001-09-19
*	changement du make depend en vu du make reals	letouzey	2001-09-10
*	2 bugs: typevarlist pour inductifs + args pour flexibles	letouzey	2001-06-22
*	mise en place extraction haskell	filliatr	2001-05-14
*	nettoyage extraction	filliatr	2001-05-09
*	make reals prend en compte tous les .vo de theories/Reals	filliatr	2001-04-25
*	TODO in v.o., test/Makefile moins pire, README avec ref	letouzey	2001-04-24
*	Ajout du .depend	mohring	2001-04-24
*	Retire theories/Num	mohring	2001-04-24
*	Fin d'optimisation (cas modules) + warning pour coind & ocaml	letouzey	2001-04-24
*	mise a jour	letouzey	2001-04-23
*	realisation des reals	letouzey	2001-04-23
*	Remaniement Makefile de test. make reals possible	letouzey	2001-04-23
*	scripts; extraction False_rec	filliatr	2001-04-19
*	blindage False_rec	filliatr	2001-04-19