coq - The formal proof system

Age	Commit message (Expand)	Author
2000-05-03	Retrait de PrintConstr vers top_printers	delahaye
2000-05-03	diverses modifs pour ocamlweb	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
2000-05-02	Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-04-27	Retrait fullmind de inductive_summary pour simplicité	herbelin
2000-04-26	Commentaires	herbelin
2000-04-21	Sign.db_signature is now an abstract type	courant
2000-04-20	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin
2000-03-30	erreurs lexicales dans les patterns (manquait des espaces)	filliatr
2000-03-21	Modification de type_of_case, type_case_branches, etc	herbelin
2000-03-21	Ajout {prod,lambda}_name	herbelin
2000-03-21	Déplacement fonction du discharge dans Discharge	herbelin
2000-03-21	Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...	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	Bug ordre des inductifs mutuels	herbelin
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	mauvais parenthesage dans hd_name (patterns imbriques)	filliatr
2000-03-16	Utilisation de l'env pour nommer les Rel	herbelin
2000-03-08	Ajout du test d'égalité des vecteurs dans convert_forall2.	herbelin
2000-03-08	Peaufinement nouveaux types inductive_summary et constructor_summary en vue	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-01-28	documentation	filliatr
2000-01-27	erreurs latex dans interfaces	filliatr
2000-01-26	MAJ ocaml 2.99 (espaces dans la syntaxe des cast)	herbelin
2000-01-26	MAJ commentaires	herbelin
2000-01-26	Abstraction de l'implémentation des signatures de Sign en vue intégration d...	herbelin
2000-01-21	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-14	clarification du code	filliatr
1999-12-13	documentation	filliatr
1999-12-13	Poursuite intégration du Cases	herbelin
1999-12-11	Intégration initiale du Cases	herbelin
1999-12-10	Suppression Rel de rawconstr et correction de bugs d'affichage	herbelin
1999-12-10	debug discharge et inductifs	filliatr
1999-12-09	Ajout des messages d'erreurs de Cases	herbelin
1999-12-09	- constantes avec recettes	filliatr
1999-12-09	Discharge (encore bugge)	filliatr
1999-12-07	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr
1999-12-07	correction bug construct_reference	filliatr
1999-12-06	check_correct_par n'etait pas fait au bon endroit	filliatr