coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-03-08	MAJ nouveau try_mutind_of	herbelin
2000-03-08	Ajout du test d'égalité des vecteurs dans convert_forall2.	herbelin
2000-03-08	Un nouveau moteur pour Cases (phase 1)	herbelin
2000-03-08	Peaufinement nouveaux types inductive_summary et constructor_summary en vue	herbelin
2000-03-07	Renommage mt_con -> empty_con	herbelin
2000-03-07	Commentaire	herbelin
2000-03-07	Export inh_conv_coerce_to et divers	herbelin
2000-03-07	Redondances	herbelin
2000-03-07	Export mis_typed_arity	herbelin
2000-03-07	Ajout destApplication	herbelin
2000-03-07	Nettoyage check_pos	herbelin
2000-03-07	Renommage ppterm0 --> ppterm	herbelin
2000-03-07	Capture des exceptions si env vide pour ne pas echouer lors du debogage	herbelin
2000-03-07	Ajout matrix_transpose	herbelin