coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	* Fixed constr_cmp again to handle universes subtyping correctly	puech	2008-10-09
*	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau	2008-10-03
*	Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an	msozeau	2008-09-04
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)	herbelin	2008-06-21
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)	barras	2008-06-05
*	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras	2008-05-28
*	refined the conversion oracle	barras	2008-05-21
*	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin	2008-05-20
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	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-27
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Bug squashing day !	msozeau	2008-04-17
*	- Relâchement de la contrainte de bonne longueur des intropatterns	herbelin	2008-04-04
*	Essai d'un peu plus de conversion dans apply : suppression de la	herbelin	2008-04-03
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01
*	Modifications diverses et variées :	herbelin	2008-03-30
*	Using the "relation" constant made some unifications fail in the new	msozeau	2008-03-16
*	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-06
*	Correction d'une typo restant du commit 10557 et cause d'échec de contribs	herbelin	2008-03-05
*	Suspension de l'introduction de delta dans apply : certaines contribs	herbelin	2008-02-14
*	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-13
*	Mise en place d'une toute petite amélioration de l'unification de	herbelin	2008-02-07
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Unification des types + clause filtrage manquante + uniformisation locale	herbelin	2007-06-07
*	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin	2007-06-06
*	Amélioration de la complexité de auto (l'utilisation des types dans	herbelin	2007-06-05
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	Unification suite: petits affinements pour préserver la compatibilité	herbelin	2007-05-24
*	Suite restructuration unification et division des problèmes	herbelin	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin	2007-05-21
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
*	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin	2007-01-22
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin	2006-10-05