coq - The formal proof system

Age	Commit message (Expand)	Author
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-03-10	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin
2008-02-08	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	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-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	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-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
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2005-12-02	Changement des named_context	gregoire
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-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2004-12-08	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin
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-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-16	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin
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
2002-11-05	Intégration des modifs de la branche mowgli :	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
2001-11-08	Introduction d'univers frais dans les types implicites engendrés par le pré...	herbelin
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-09-14	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin
2001-09-09	Préparation du prétypage à la mise en place d'univers algébriques	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-10	Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)	herbelin
2001-03-29	deux fois $Id$	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-11-27	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-10-23	Petit nettoyage de Evarutil et Evarconv	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin