coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-12-09	Achèvement correction bug do_restrict_hys: ne pas inverser les arguments	herbelin
2004-12-08	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin
2004-12-06	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-08	unification encore...	barras
2004-09-08	petit bug avec les effets de bords	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-13	bug #794: conv made in wrong env	barras
2004-07-13	bug #790: better error_not_clean	barras
2004-06-30	updated printing of evar context (may loop ?)	corbinea
2004-01-29	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-04-11	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-12	petite modif pour ne pas expanser trop de let pendant l'unification	barras