coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin	2004-12-06
*	Commentaire	herbelin	2004-12-06
*	Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...	herbelin	2004-12-03
*	UserError in reduce_to_*_ref	herbelin	2004-11-29
*	Correction bug #879	herbelin	2004-11-26
*	MAJ PCoFix	herbelin	2004-11-26
*	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin	2004-11-19
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Vérification de la typability de 'pattern'	herbelin	2004-10-17
*	?(mod_delta=true) parameter added to each unification function.	sacerdot	2004-09-27
*	collapse apps of patterns to avoid failures	barras	2004-09-27
*	Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...	herbelin	2004-09-25
*	error if binder was already defined	barras	2004-09-23
*	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
*	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