coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fixed a bug in checking that implicit arguments are all correctly	herbelin	2009-09-18
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	Backtrack on experimental unification with sort variables: it requires	msozeau	2009-06-02
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	Minor unification changes:	msozeau	2009-05-18
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau	2008-12-14
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	More debugging of handling of open constrs with typeclasses:	msozeau	2008-10-25
*	Raise informative errors instead of Failures or anomalies in case a meta	msozeau	2008-10-24
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin	2008-04-27
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Bug squashing day !	msozeau	2008-04-17
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Using the "relation" constant made some unifications fail in the new	msozeau	2008-03-16
*	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin	2008-02-13
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10
*	Changement des named_context	gregoire	2005-12-02
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	simplification de clenv	barras	2004-09-10
*	unification encore...	barras	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03