coq - The formal proof system

Age	Commit message (Expand)	Author
2011-05-05	Fix merge, Cumul moved to CUMUL	msozeau
2011-05-05	Merge branch 'subclasses' into coq-trunk	msozeau
2011-05-04	First phase removing obsolete support for eta up to conversion in	herbelin
2011-04-20	Allow betaiota when checking unification of the types of metas (fixes ATBR co...	msozeau
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-04-16	Fix unification of types of metavariables and error message for sort unificat...	msozeau
2011-04-13	- 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-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