coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Refined second_order_matching so that a constraint on which	herbelin	2011-11-08
*	optimization: memoization for is_open_canonical_projection	gareuselesinge	2011-11-08
*	Improved check is_open_canonical_projection	gareuselesinge	2011-11-08
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Deactivating second-order pattern-matching in evarconv for 8.4.	herbelin	2011-10-26
*	Fixing instance/filter mismatch in materialize_evar + documentation.	herbelin	2011-10-24
*	Fail if some conv pbs remain after consider_remaining_unif_problems.	herbelin	2011-10-22
*	Use also second-order unification if first-order fails at the time of conside...	herbelin	2011-10-22
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Evarconv: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Applying Enrico Tassi's patch for giving priority to delta over eta in	herbelin	2011-05-24
*	As remarked by Enrico, we'd better use eq_constr than structural equality	herbelin	2011-03-31
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Revert commit r13883: instantiating ?n by a lambda when "?n a" has to	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added support for instantiation of ?n by a lambda when "?n a" has to	herbelin	2011-03-05
*	Reorganized a bit evarconv.ml:	herbelin	2011-03-05
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Fix bug 2307	pboutill	2010-05-20
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	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
*	Fix treatment of remaining unification constraints: raise a more	msozeau	2010-03-07
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin	2009-08-11
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	change in the order of unification constraints solving (for canonical structu...	amahboub	2009-07-06
*	Backtrack on experimental unification with sort variables: it requires	msozeau	2009-06-02
*	Properly catch sort constraint inconsistency exception in	msozeau	2009-05-28
*	Populate the sort constraints set correctly during unification. Add a	msozeau	2009-05-27
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	fix a bug in canonical structures (bug found and fixed by Cyril)	barras	2009-05-09
*	Fixes to make Ynot compile with the trunk:	msozeau	2009-03-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
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	fixed problem with r11612	barras	2008-11-21
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07