coq - The formal proof system

Age	Commit message (Expand)	Author
2008-02-11	Correction d'un bug de clear	notin
2008-02-10	Fixing bug 1795 (occur check was not correctly done)	herbelin
2008-02-08	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau
2008-01-21	Correction du bug #1754	notin
2008-01-18	Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...	msozeau
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-18	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-16	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-09-04	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin
2007-09-01	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin
2007-08-29	Prise en compte des redéfinitions de variables (définitions locales	herbelin
2007-08-25	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-03-27	Modification de la vm:	notin
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-01-31	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin
2007-01-30	Nouvelle implantation de clear_hyps	notin
2007-01-22	Correction du bug #1315:	notin
2006-12-12	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-11-18	Code mort (duplication de code dans reductionops.ml)	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-12	Ajout unification pattern dans l'algorithme d'unification des	herbelin
2006-08-29	Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis	herbelin
2006-08-29	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin
2006-08-28	Diverses modifications autour de l'unification modulo conversion:	herbelin
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-10	Fixes for new unification, not used in default version as it really changes u...	msozeau
2006-04-10	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau
2006-04-07	- Documentation of the Program tactics.	msozeau
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-06-09	backtrack sur le typage des instantiations d\'evars	barras
2005-06-07	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras
2005-06-06	essai de typage des instantiations d\'evars	barras
2005-06-05	eradication de Evarutil.w_Define	barras
2005-06-05	assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...	barras
2005-05-28	unification: evar_define checks the free variables are bound in the evar context	barras
2005-05-24	WARNING: unification changed (to fix a bug).	sacerdot
2005-03-12	Backtrack version 1.82 awaiting for better understanding of the consequences ...	herbelin
2005-03-11	Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...	herbelin
2005-03-09	bug #931 (continued): no recursion on the evars instantiation	herbelin
2005-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2005-03-01	Code mort	herbelin