coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Backtrack sur la mémoïsation de nf_evar.	aspiwack	2009-03-04
*	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack	2009-02-27
*	On passe les last_mods (un des champs de Evd.evar_defs) de list	aspiwack	2009-02-20
*	On ne met plus rien dans les last_mods tant que conv_pbs est vide.	aspiwack	2009-02-20
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	memoized is_ground_env	barras	2009-02-09
*	pushed evar reduction in kernel	barras	2009-02-06
*	From v8.2 to trunk:	herbelin	2009-02-06
*	Really compare evar maps in progress, due to merging in apply and other	msozeau	2009-01-23
*	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin	2009-01-20
*	- Fixing bug 1891 (abusive instantiations of evar arguments in	herbelin	2009-01-20
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	Correct a bug in commit 11659	puech	2009-01-16
*	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau	2009-01-12
*	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin	2009-01-05
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Fixed two apparent inconsistencies in matching.ml:	herbelin	2009-01-02
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin	2008-12-26
*	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech	2008-12-06
*	Fixes for unification and substitution of metas under binders.	msozeau	2008-12-04
*	improved simpl	barras	2008-12-03
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	another bug with simpl	barras	2008-11-28
*	Fix (?) a pattern matching compilation problem:	msozeau	2008-11-27
*	fixed bug 1791: simpl was performing eta expansion	barras	2008-11-27
*	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras	2008-11-27
*	fixed problem with r11612	barras	2008-11-21
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
*	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey	2008-11-14
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Apply vmconv if there are no _undefined_ evars around.	msozeau	2008-11-08
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	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
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Retour en arrière pour raison de compatibilité sur la suppression du nf_evar	herbelin	2008-10-19
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	* Fixed constr_cmp again to handle universes subtyping correctly	puech	2008-10-09
*	fixing r11433 again:	barras	2008-10-07
*	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau	2008-10-03
*	Fixing constr_cmp, propagating subtyping only right of a product	puech	2008-10-02
*	Correcting a delta normalization bug in VM (checked by benjamin)	jforest	2008-09-30