coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin	2009-07-15
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau	2009-06-30
*	Fix "unsatisfiable constraints" error messages to include all the	msozeau	2009-06-18
*	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
*	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
*	Temporary fixes in unification:	msozeau	2009-05-24
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	Many fixes in unification:	msozeau	2009-05-20
*	Fix in canonical structure resolution: [check_conv_record] may return	msozeau	2009-05-19