coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-04-27	Quelques bricoles autour de l'unification:	herbelin
2008-04-27	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin
2008-04-27	- Fix bug in unification not taking into account the right meta	msozeau
2008-04-26	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-17	Bug squashing day !	msozeau
2008-04-04	- Relâchement de la contrainte de bonne longueur des intropatterns	herbelin
2008-04-03	Essai d'un peu plus de conversion dans apply : suppression de la	herbelin
2008-04-01	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin
2008-03-30	Modifications diverses et variées :	herbelin
2008-03-16	Using the "relation" constant made some unifications fail in the new	msozeau
2008-03-06	Toujours suite commits 10623 et 10624:	herbelin
2008-03-06	Suite commit 10623:	herbelin
2008-03-06	Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n	herbelin
2008-03-05	Correction d'une typo restant du commit 10557 et cause d'échec de contribs	herbelin
2008-02-14	Suspension de l'introduction de delta dans apply : certaines contribs	herbelin
2008-02-13	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin
2008-02-13	Correction de ce qui semble être un petit bug dans la gestion de la	herbelin
2008-02-07	Mise en place d'une toute petite amélioration de l'unification de	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-06-07	Unification des types + clause filtrage manquante + uniformisation locale	herbelin
2007-06-06	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin
2007-06-05	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin