coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Orthographe de 'instantiate'	herbelin	2005-12-17
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	backtrack sur le typage des instantiations d\'evars	barras	2005-06-09
*	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
*	assouplissement de real_clean: ne tient pas compte des occcurences flexibles ...	barras	2005-06-05
*	unification: evar_define checks the free variables are bound in the evar context	barras	2005-05-28
*	WARNING: unification changed (to fix a bug).	sacerdot	2005-05-24
*	Backtrack version 1.82 awaiting for better understanding of the consequences ...	herbelin	2005-03-12
*	Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendant...	herbelin	2005-03-11
*	bug #931 (continued): no recursion on the evars instantiation	herbelin	2005-03-09
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Code mort	herbelin	2005-03-01
*	Achèvement correction bug do_restrict_hys: ne pas inverser les arguments	herbelin	2004-12-09
*	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin	2004-12-08
*	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin	2004-12-06
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	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
*	unification encore...	barras	2004-09-08
*	petit bug avec les effets de bords	barras	2004-09-08
*	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
*	bug #794: conv made in wrong env	barras	2004-07-13
*	bug #790: better error_not_clean	barras	2004-07-13
*	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
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	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
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	petite modif pour ne pas expanser trop de let pendant l'unification	barras	2002-02-12
*	substitution et pattern modulo let	barras	2002-02-11
*	compat ocaml 3.03	filliatr	2001-12-13
*	Bug mauvaise instance	herbelin	2001-11-20
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
*	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
*	Passage aux univers algébriques	herbelin	2001-09-09
*	Préparation du prétypage à la mise en place d'univers algébriques	herbelin	2001-09-09
*	has_undefined_isevars était buggé	herbelin	2001-07-06
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23