coq - The formal proof system

Age	Commit message (Expand)	Author
2000-03-23	Amélioration d'un message d'erreur	herbelin
2000-03-21	- bug make_module_marker (plus de # et de .obj maintenant)	filliatr
2000-03-21	Modification de type_of_case, type_case_branches, etc	herbelin
2000-03-21	Nettoyage	herbelin
2000-03-21	Modification de type_of_case, type_case_branches, etc;nettoyage	herbelin
2000-03-21	Ajout {prod,lambda}_name	herbelin
2000-03-21	Retour sur les anciens noms	herbelin
2000-03-21	MAJ	herbelin
2000-03-21	MAJ ocaml 2.99	herbelin
2000-03-21	MAJ	herbelin
2000-03-21	Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...	herbelin
2000-03-21	Prise en compte nouveau case_info	herbelin
2000-03-21	Déplacement des fonctions spécifiques du discharge qui était dans Generic;...	herbelin
2000-03-21	Déplacement fonction du discharge dans Discharge	herbelin
2000-03-21	Remplacement plain_instance en instance qui n'a plus besoin de env	herbelin
2000-03-21	Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...	herbelin
2000-03-21	Plus besoin de env dans reduce_mind_case	herbelin
2000-03-21	Prise en compte nouveau case_info et nouvel Reduction.instance	herbelin
2000-03-21	Inlining prod_create	herbelin
2000-03-21	Prise en compte nouveau case_info dans type_case	herbelin
2000-03-21	Prise en compte nouveau case_info	herbelin
2000-03-21	Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et...	herbelin
2000-03-21	Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...	herbelin
2000-03-20	Tauto	filliatr
2000-03-20	Affichage des <> pour débug	herbelin
2000-03-20	Bug ordre des inductifs mutuels	herbelin
2000-03-20	Affichage des anonymes si lambda	herbelin
2000-03-18	ZArith	filliatr
2000-03-18	Zarith	filliatr
2000-03-18	on ne compile pas Div.v (Realizer)	filliatr
2000-03-18	g_natsyntax.ml	filliatr
2000-03-18	bug discharge (work_alist contenanti plein de fois les memes choses)	filliatr
2000-03-17	Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'	herbelin
2000-03-17	Un cast inutile	herbelin
2000-03-16	Syntactic Definition n'etaient pas correctemenet importees	filliatr
2000-03-16	theories/Bool	filliatr
2000-03-16	mise sous CVS	filliatr
2000-03-16	mauvais parenthesage dans hd_name (patterns imbriques)	filliatr
2000-03-16	Utilisation de l'env pour nommer les Rel	herbelin
2000-03-16	Qqes bugs (evars dans le predicat; tag des cas défauts)	herbelin
2000-03-10	Eqdep_dec doit etre compile	filliatr
2000-03-10	t -> $t dans regle grammaire EX	filliatr
2000-03-10	compilation theories/Arith	filliatr
2000-03-10	mise sous CVS du repertoire theories/Arith	filliatr
2000-03-10	* empty log message *	barras
2000-03-10	Reparation bug isevars dans pretyping	herbelin
2000-03-08	Ajout theories/Logic/*.vo	herbelin
2000-03-08	MAJ	herbelin
2000-03-08	La partie 'val' de trad_constraints devient un typed_type	herbelin
2000-03-08	Réparation du cast oublié lors d'une définition castée	herbelin