coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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-03-18
*	added isProd to term.mli.	coq	2006-02-16
*	Variable inutilisée	herbelin	2006-01-21
*	* empty log message *	barras	2006-01-20
*	Suppression résidus code v7 et traducteur	herbelin	2006-01-11
*	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	2006-01-10
*	Uniformisation: extension de la suppression d'un casts dans collapse_app à l...	herbelin	2005-12-21
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Orthographe de 'instantiate'	herbelin	2005-12-17
*	j'avais oublie ces deux fichiers.	gregoire	2005-12-06
*	correction bug 881.	gregoire	2005-12-05
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	parametres inductifs	mohring	2005-11-28
*	bug #909: Top n'est cree que si le contexte est vide	barras	2005-11-23
*	petites corrections + contournement bug projections	barras	2005-11-18
*	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-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Suppression code inactif et commentaire apparemment incorrect (pour éviter c...	herbelin	2005-09-09
*	Simplification message d'anomalie	herbelin	2005-09-08
*	argument inutilisÃ© de zip: toujours l'identitÃ©	letouzey	2005-08-22