coq - The formal proof system

Age	Commit message (Expand)	Author
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-03-08	Solve evar instantiations in the right environment.	msozeau
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-02-17	- Use transparency information all the way through unification and	msozeau
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-11-07	Delayed the evar normalization in error messages to the last minute	herbelin
2010-09-30	Improve handling of metas as evars in unification (patch by Hugo)	letouzey
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-25	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin
2010-06-18	Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).	herbelin
2010-06-12	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin
2010-05-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-11	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin
2010-04-05	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-03-07	Fix treatment of remaining unification constraints: raise a more	msozeau
2010-02-22	Improve unification when evars and metas are mixed.	msozeau
2010-01-26	Quick fix for references to section variables unbound in the current	msozeau
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-02	Backtrack on experimental unification with sort variables: it requires	msozeau
2009-06-01	Change unification with sort constraints to not use the kernel	msozeau
2009-05-28	Properly catch sort constraint inconsistency exception in	msozeau
2009-05-27	Populate the sort constraints set correctly during unification. Add a	msozeau
2009-05-24	Temporary fixes in unification:	msozeau
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-20	Many fixes in unification:	msozeau
2009-05-19	Fix in canonical structure resolution: [check_conv_record] may return	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-05-16	(Tentative to) add Canonical Structure resolution to the regular	msozeau
2009-04-09	Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use	herbelin
2009-04-08	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-06	pushed evar reduction in kernel	barras
2009-01-20	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin
2009-01-12	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau