coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin	2008-03-15
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	Unification des types + clause filtrage manquante + uniformisation locale	herbelin	2007-06-07
*	Correction pour le rapport de bug #1325 par rétablissement du	herbelin	2007-01-22
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin	2006-05-28
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
*	Changement des named_context	gregoire	2005-12-02
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	test de conversion laissait echapper exception NotConvertible	barras	2004-05-14
*	Commentaires	herbelin	2002-12-10
*	Essai suppression nf_betaiota dans type_of	herbelin	2002-12-09
*	petite erreur dans le typage des let-in	barras	2002-03-28
*	typage du produit: type_judgment appele avec contexte incorrect	barras	2002-02-19
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...	herbelin	2001-11-08
*	GROS COMMIT:	barras	2001-11-05
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Changement de la structure des points fixes	barras	2001-05-03
*	entetes	filliatr	2001-03-15
*	nouvelle implantation de la reduction	barras	2001-03-01
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage	herbelin	2000-11-29
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	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
*	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
*	Bricoles	herbelin	2000-06-29
*	Rattrapage d'un Not_found pour les VAR's.	delahaye	2000-06-28
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
*	Nettoyage de Generic	herbelin	2000-05-31
*	Prise en compte nouveau case_info	herbelin	2000-03-21