coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin	2009-04-08
*	- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing	herbelin	2009-04-08
*	Fix obvious bug in evars_of_named_context.	msozeau	2009-04-03
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fix bug #2056 (discharge bug).	msozeau	2009-03-28
*	Compromise wrt introduction-names compatibility issue after addition	herbelin	2009-03-22
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Fixes to make Ynot compile with the trunk:	msozeau	2009-03-20
*	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