coq - The formal proof system

Age	Commit message (Expand)	Author
2007-01-19	Prise en compte des univers algébriques dans les types inférés dans	herbelin
2007-01-19	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin
2007-01-17	Correction bug #1302	herbelin
2006-12-12	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin
2006-12-12	cosmetique	barras
2006-12-11	Changement dans le kernel :	bgregoir
2006-12-08	bug condition de garde	barras
2006-10-30	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin
2006-10-30	dependences	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-27	Ajout fold_rel_declaration et fold_named_declaration	herbelin
2006-10-27	Correction de 2 bugs critiques du polymorphisme d'univers	herbelin
2006-10-27	changement des _sym par _comm dans setoid_ring	bgregoir
2006-10-17	Clarification des contraintes sur le contexte de paramètres des	herbelin
2006-10-12	Protection raise en début de séquence (en attendant que le code caché trou...	herbelin
2006-10-06	Déplacement de on_judgment_type de Typeops vers Termops	herbelin
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-10-03	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin
2006-09-14	Correction du bug #1181	jforest
2006-09-01	Indentation + typo	notin
2006-09-01	Ajout iter_rel_context/iter_named_context	herbelin
2006-09-01	Appel à caml_modify pour Ocaml 3.07	notin
2006-08-28	Export de closedn pour Evarutil	herbelin
2006-08-25	correction bug vm_compute	bgregoir
2006-07-28	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2006-06-22	Correction bug du polymorphisme de sort des inductifs (cas où les variables ...	herbelin
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