coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin	2008-05-20
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin	2008-03-10
*	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau	2008-02-08
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin	2007-01-31
*	Nouvelle implantation de clear_hyps	notin	2007-01-30
*	Correction du bug #1315:	notin	2007-01-22
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Ajout unification pattern dans l'algorithme d'unification des	herbelin	2006-09-12
*	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin	2006-08-29
*	Diverses modifications autour de l'unification modulo conversion:	herbelin	2006-08-28
*	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-10
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Changement des named_context	gregoire	2005-12-02
*	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras	2005-06-07
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	eradication de Evarutil.w_Define	barras	2005-06-05
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin	2004-12-08
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin	2004-07-16
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin	2004-01-29
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...	herbelin	2002-04-11
*	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin	2002-04-10
*	Introduction d'univers frais dans les types implicites engendrés par le pré...	herbelin	2001-11-08
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	GROS COMMIT:	barras	2001-11-05
*	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin	2001-09-14
*	Préparation du prétypage à la mise en place d'univers algébriques	herbelin	2001-09-09
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)	herbelin	2001-05-10
*	deux fois $Id$	filliatr	2001-03-29
*	amelioration de la structure des univers	barras	2001-03-28
*	entetes	filliatr	2001-03-15
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Branchement du mécanisme d'instantiation des Evar en présence de définitio...	herbelin	2000-11-27
*	correction Abstract (et make world passe!)	filliatr	2000-11-02