coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	simplification de clenv	barras	2004-09-10
*	unification encore...	barras	2004-09-08
*	petit bug avec les effets de bords	barras	2004-09-08
*	Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...	herbelin	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	mimick: unify types before making assignation	barras	2004-09-06
*	bad env in mimick code	barras	2004-09-06
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...	herbelin	2004-08-24
*	Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...	herbelin	2004-08-24
*	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin	2004-08-24
*	Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...	herbelin	2004-08-24
*	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin	2004-08-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suppression de Rawterm.loc, branchement sur Util.loc	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
*	Eta-expansion du predicat dans build_indrec (suite)	herbelin	2004-07-11
*	Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...	herbelin	2004-07-11
*	Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...	herbelin	2004-07-11
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Essai de suppression de eta dans simpl (cf bug #779)	herbelin	2004-06-29
*	Double bug d'affichage des cases dépendants (bug #784)	herbelin	2004-06-28
*	Correction affichage v8 des records avec let (bug #798)	herbelin	2004-06-27
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	test de conversion laissait echapper exception NotConvertible	barras	2004-05-14
*	Terminologie plus intuitive: evaluable -> unfoldable	herbelin	2004-04-30
*	Prise en compte d'un type dont la sorte est une evar	herbelin	2004-04-29
*	Correction incapacité à gérer les annotations de type dépendantes pour le...	herbelin	2004-04-27
*	Correction confusion entre la dependance en les termes filtrees dans l'annota...	herbelin	2004-04-13
*	bug #606: mis un message d'erreur plus clair	barras	2004-04-07
*	Déclaration des record au chargement (ce n'est pas une question de visibilit...	herbelin	2004-04-05
*	Typo	herbelin	2004-03-29
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin	2004-03-28
*	bug de PP des fix (coqbugs #574)	barras	2004-03-24
*	preparation pour release (suite)	barras	2004-03-15
*	bug affichage des cofix	barras	2004-03-09
*	correction de bugs des points fixes	barras	2004-03-08
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Erreur de Bruijn et oubli substitution alias dans annotation du 'match'	herbelin	2004-02-27
*	Inclusion des annotations de type des filtrages dans 'Set Printing All'	herbelin	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (suite)	herbelin	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...	herbelin	2004-02-13
*	On s'affranchit de l'information inductif ou pas dans le prédicat (càd	herbelin	2004-02-05
*	Suppression des types dans la signature du predicat (ils sont	herbelin	2004-02-05