coq - The formal proof system

Age	Commit message (Expand)	Author
2000-05-22	Renommage hypothèses de nom redondant dans les environnements	herbelin
2000-05-22	suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls	herbelin
2000-05-22	Changement nom module Constant en Declarations	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin
2000-05-18	MAJ modifs Inductive	herbelin
2000-05-18	Ajouts des causes d'erreur de Indrec	herbelin
2000-05-18	Restructuration des outils pour les inductifs.	herbelin
2000-05-18	Ajout lift_context	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-18	Centralisation prod_name and co dans Environ; mkLambda_string dans Term	herbelin
2000-05-18	Restructuration des outils pour les inductifs.	herbelin
2000-05-18	Centralisation prod_name and co dans Environ; mkLambda_string dans Term	herbelin
2000-05-16	Ajout mis_typepath	herbelin
2000-05-05	doc	herbelin
2000-05-05	Ajout d'un strong 'light'	herbelin
2000-05-04	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin
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