coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras	2005-06-07
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Correction bug #879	herbelin	2004-11-26
*	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin	2004-11-19
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	Unification plus efficace vis à vis du LetIn	herbelin	2003-01-31
*	reparation des contribs: lors de l'unification, reduire les beta redexes	barras	2003-01-23
*	modified the unification algorithm to try first order unification before	barras	2003-01-22
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	L'ordre supérieur avait quelque peu été oublié dans l'unification...	herbelin	2002-06-07
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin	2002-04-11
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue	barras	2002-02-18
*	GROS COMMIT:	barras	2001-11-05
*	Amérioration message d'erreur en cas d'échec du filtrage de premier ordre	herbelin	2001-10-29
*	Nettoyage Recordobj et conséquences	herbelin	2001-10-16
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	la conversion ne doit être testé dans evar_conv qu'en absence de evar	herbelin	2001-07-06
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Modification pour passage p-automates	mohring	2001-05-15
*	Changement de la structure des points fixes	barras	2001-05-03
*	Bug context incoherent au passage du lambda et du let dans evar_eqappr	herbelin	2001-04-10
*	amelioration de la structure des univers	barras	2001-03-28
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	entetes	filliatr	2001-03-15
*	nouvelle implantation de la reduction	barras	2001-03-01
*	Bug de contextes	herbelin	2000-12-26
*	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin	2000-12-26
*	Utilisation de Let In pour les constantes locales, prise en compte des Let In...	herbelin	2000-11-27
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Petit nettoyage de Evarutil et Evarconv	herbelin	2000-10-23
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Renommage AppL en App	herbelin	2000-10-01
*	Abstraction de constr	herbelin	2000-09-14
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Correction pour make doc	herbelin	2000-09-10
*	Suppression de Abst	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Achèvement abstraction du mécanisme (optionnel) de cast	herbelin	2000-06-29