coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Continuing r14585 (ill-typed restriction bug).	herbelin	2011-10-25
*	Continuing r1492 (useless changes were inadvertantly committed)	herbelin	2011-10-25
*	New strategy to infer return predicate of match construct when	herbelin	2011-10-25
*	Fixing another bug revealing ill-typed use of evar restriction.	herbelin	2011-10-24
*	Fixing instance/filter mismatch in materialize_evar + documentation.	herbelin	2011-10-24
*	Partly reverting r14539 about fully expanding "let-in"s and not just	herbelin	2011-10-17
*	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
*	Fixing buggy abberant code for Evarutil.expand_evar	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	Fix nf_evars_undefined	msozeau	2011-08-03
*	Evarutil: replace generic list_distinct on constr by constr_list_distinct	puech	2011-07-29
*	Evarutil: replaced some generic = on constr by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by destructors	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech	2011-07-29
*	Evarutil: generic equality on constr replaced by eq_constr	puech	2011-07-29
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
*	Fixes in pruning, do not fail if pruning is impossible due to typing constrai...	msozeau	2011-06-10
*	More fixes in pruning/restriction of evars during unification.	msozeau	2011-06-09
*	Fixes in pruning in unification.	msozeau	2011-06-08
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Catch NotArity exception and transform it into an anomaly in retyping.	msozeau	2011-04-11
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau	2011-03-23
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Instantiate evar by a lambda when "?n args" has to unify with Prod	herbelin	2011-03-05
*	In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)	letouzey	2011-02-11
*	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey	2011-02-03
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Speed-up refine by avoiding some calls to Evd.fold	letouzey	2010-09-30
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Added rudimentary support for using constructors from the explicit	herbelin	2010-06-12
*	Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).	herbelin	2010-06-12
*	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin	2010-06-11
*	Fixing Derive Inversion for new proof engine	herbelin	2010-05-26
*	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
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Fixed bugs from commit 12954 on unification complexity	herbelin	2010-04-20
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19