coq - The formal proof system

Age	Commit message (Expand)	Author
2006-06-05	Oh le joli bug dans le kernel:	letouzey
2006-05-30	retour au comportement antérieur pour une application de foncteur:	letouzey
2006-05-28	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin
2006-05-23	Modification de add_glob (support des modules dans Coqdoc)	notin
2006-05-23	Ajout substl_named_decl pour mode Maple	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-13	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin
2006-05-12	correction bugs de condition de garde (fix + cofix)	barras
2006-05-10	correction bugs dans Cbv (beta n-aire)	barras
2006-05-09	subst. explicites avec vecteurs	barras
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-05-03	fixed bug #804: removed useless reduction in fix guard checking	barras
2006-05-03	bug #1096: whd_stack on one arg of conversion had side-effect on the other arg	barras
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-16	Nouveau mécanisme pour les modules interactifs : les arguments de	herbelin
2006-04-15	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin
2006-03-29	Inductifs avec polymorphisme de sorte (version initiale)	herbelin
2006-03-22	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin
2006-03-18	MAJ documentation en syntaxe v8	herbelin
2006-03-18	Documentation mutual_inductive_body	herbelin
2006-03-18	Bug calcul consnrealargs + bug calcul occurrences non positives + modifs cosm...	herbelin
2006-02-16	added isProd to term.mli.	coq
2006-01-21	Variable inutilisée	herbelin
2006-01-20	* empty log message *	barras
2006-01-11	Suppression résidus code v7 et traducteur	herbelin
2006-01-10	Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...	herbelin
2006-01-10	Détection var inutile par ocaml 3.09	herbelin
2005-12-21	Uniformisation: extension de la suppression d'un casts dans collapse_app à l...	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-12-06	j'avais oublie ces deux fichiers.	gregoire
2005-12-05	correction bug 881.	gregoire
2005-12-05	changement d'egalite pour le named_context_val	gregoire
2005-12-02	Changement des named_context	gregoire
2005-11-28	parametres inductifs	mohring
2005-11-23	bug #909: Top n'est cree que si le contexte est vide	barras
2005-11-18	petites corrections + contournement bug projections	barras
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-08	Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09	herbelin
2005-11-08	Nettoyage suite nouvel avertissement Z de ocaml 3.09	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-09-09	Suppression code inactif et commentaire apparemment incorrect (pour éviter c...	herbelin
2005-09-08	Simplification message d'anomalie	herbelin
2005-08-22	argument inutilisÃ© de zip: toujours l'identitÃ©	letouzey
2005-08-19	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey
2005-07-21	Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...	herbelin
2005-07-13	reactivation de l optim des fermetures	barras
2005-07-13	backtrack modif de knh...	barras
2005-07-13	* empty log message *	barras