coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	Various improvements in handling of evars in general and typing	msozeau	2008-06-21
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
*	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin	2006-10-06
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Fixes for new unification, not used in default version as it really changes u...	msozeau	2006-04-10
*	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau	2006-04-10
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	Localisation des erreurs de sorte du prétypage	herbelin	2006-02-08
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	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
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin	2002-04-11
*	Mise en place de coercion dans les motifs	herbelin	2001-12-11
*	GROS COMMIT:	barras	2001-11-05
*	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin	2001-09-14
*	bug de Bruijn	herbelin	2001-08-13
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Bug environnement	herbelin	2001-01-11
*	Insertion de coercion au milieu des applications partielles et propagation de...	herbelin	2000-11-08
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Petit nettoyage de Evarutil et Evarconv	herbelin	2000-10-23
*	Nettoyage Coercion	herbelin	2000-10-19
*	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
*	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
*	Amelioration messages erreurs	herbelin	2000-06-09
*	bugs et simplification (suite)	herbelin	2000-06-02
*	Bugs et simplifications coercions	herbelin	2000-06-02
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01