coq - The formal proof system

Age	Commit message (Expand)	Author
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
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-04	Fixes for unification and substitution of metas under binders.	msozeau
2008-12-02	Miscellaneous fixes and improvements:	herbelin
2008-11-14	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey
2008-11-05	Fix in the unification algorithm using evars: unify types of evar	msozeau
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-10-09	* Fixed constr_cmp again to handle universes subtyping correctly	puech
2008-10-03	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau
2008-09-04	Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-21	Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)	herbelin
2008-06-18	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-05	changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)	barras
2008-05-28	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras
2008-05-21	refined the conversion oracle	barras
2008-05-20	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin
2008-04-28	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau