coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Petite correction sur un message d'erreur renvoyé au sous typage.	soubiran	2007-01-30
*	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran	2007-01-24
*	Correction du bug #1315:	notin	2007-01-22
*	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-19
*	Correction bug #1302	herbelin	2007-01-17
*	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin	2006-12-12
*	cosmetique	barras	2006-12-12
*	Changement dans le kernel :	bgregoir	2006-12-11
*	bug condition de garde	barras	2006-12-08
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	dependences	barras	2006-10-30
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	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-27
*	Clarification des contraintes sur le contexte de paramètres des	herbelin	2006-10-17
*	Protection raise en début de séquence (en attendant que le code caché trou...	herbelin	2006-10-12
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin	2006-10-03
*	Correction du bug #1181	jforest	2006-09-14
*	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-09-01
*	Export de closedn pour Evarutil	herbelin	2006-08-28
*	correction bug vm_compute	bgregoir	2006-08-25
*	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin	2006-07-28
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Correction bug du polymorphisme de sort des inductifs (cas où les variables ...	herbelin	2006-06-22
*	Oh le joli bug dans le kernel:	letouzey	2006-06-05
*	retour au comportement antérieur pour une application de foncteur:	letouzey	2006-05-30
*	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin	2006-05-28
*	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-23
*	Correction trou de typage des éliminations d'inductifs introduit dans commit...	herbelin	2006-05-13
*	correction bugs de condition de garde (fix + cofix)	barras	2006-05-12
*	correction bugs dans Cbv (beta n-aire)	barras	2006-05-10
*	subst. explicites avec vecteurs	barras	2006-05-09
*	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras	2006-05-05
*	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-05-03
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Nouveau mécanisme pour les modules interactifs : les arguments de	herbelin	2006-04-16
*	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin	2006-04-15
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
*	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin	2006-03-22