coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Continuing r14585 (ill-typed restriction bug).	herbelin	2011-10-25
*	Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...	herbelin	2011-10-22
*	More on r14536 (an unused pattern-matching remained in the commit).	herbelin	2011-10-11
*	Little code simplification of instantiate_evar in evd.ml	herbelin	2011-10-10
*	Added information about evar origin in pretty-printing evd for debug	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	More robust evar_map debugging printer	herbelin	2011-08-02
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	A better procedure for checking presence of undefined evars.	aspiwack	2011-05-13
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04
*	- Remove useless grammar rule	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
*	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau	2011-03-10
*	Do not forget conv_pbs when resetting an evm:	msozeau	2011-03-10
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin	2010-06-22
*	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin	2010-06-12
*	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
*	Stop dropping evar constraints when building a new goal evar defs.	msozeau	2010-03-15
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Attached evar source to the evar_info and add location to tclWITHHOLES errors	herbelin	2009-12-22
*	In "progress", extending the set of evars w/o solving an existing one is	herbelin	2009-12-21
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Backtrack on experimental unification with sort variables: it requires	msozeau	2009-06-02
*	Change unification with sort constraints to not use the kernel	msozeau	2009-06-01
*	Populate the sort constraints set correctly during unification. Add a	msozeau	2009-05-27
*	Temporary fixes in unification:	msozeau	2009-05-24
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin	2009-04-08
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	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