coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing two typos introduced in r14217 and r14223	herbelin	2011-06-20
*	Ensured that the transparency state is used when flag betaiota is on for apply.	herbelin	2011-06-19
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Activating flags betaiota by default for apply	herbelin	2011-06-18
*	The ad hoc version for first-order unification at toplevel of "?n args	herbelin	2011-06-18
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Oups, typo in previous commit	herbelin	2011-06-12
*	Removed what looks like a (very old) useless f.o. unification pass	herbelin	2011-06-12
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Fix merge, Cumul moved to CUMUL	msozeau	2011-05-05
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04
*	Allow betaiota when checking unification of the types of metas (fixes ATBR co...	msozeau	2011-04-20
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Fix unification of types of metavariables and error message for sort unificat...	msozeau	2011-04-16
*	- Remove create_evar_defs	msozeau	2011-04-13
*	- Improve unification (beta-reduction, and same heuristic as evarconv for red...	msozeau	2011-04-13
*	Unify meta types with the right flags, add betaiotazeta reduction to unificat...	msozeau	2011-04-13
*	Proper typing of metavariables, type errors were completely ignored before......	msozeau	2011-04-13
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Solve evar instantiations in the right environment.	msozeau	2011-03-08
*	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
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Improve handling of metas as evars in unification (patch by Hugo)	letouzey	2010-09-30
*	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
*	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin	2010-06-25
*	Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).	herbelin	2010-06-18
*	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
*	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin	2010-04-11
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Granting wish #2251 (forbidding rewriting a term reduced to an evar)	herbelin	2010-04-05
*	Partial fix to bug #2244 (ensure that pattern unification does not	herbelin	2010-04-05
*	Fix treatment of remaining unification constraints: raise a more	msozeau	2010-03-07
*	Improve unification when evars and metas are mixed.	msozeau	2010-02-22
*	Quick fix for references to section variables unbound in the current	msozeau	2010-01-26
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Changed the way to support compatibility with previous versions.	herbelin	2009-10-04
*	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
*	Improved parameterization of Coq:	herbelin	2009-08-02