coq - The formal proof system

Age	Commit message (Expand)	Author
2004-12-06	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin
2004-12-06	Commentaire	herbelin
2004-12-03	Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...	herbelin
2004-11-29	UserError in reduce_to_*_ref	herbelin
2004-11-26	Correction bug #879	herbelin
2004-11-26	MAJ PCoFix	herbelin
2004-11-19	Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE	herbelin
2004-11-16	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-12	Changement dans les boxed values .	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-17	Vérification de la typability de 'pattern'	herbelin
2004-09-27	?(mod_delta=true) parameter added to each unification function.	sacerdot
2004-09-27	collapse apps of patterns to avoid failures	barras
2004-09-25	Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...	herbelin
2004-09-23	error if binder was already defined	barras
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-10	simplification de clenv	barras
2004-09-08	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-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-06	mimick: unify types before making assignation	barras
2004-09-06	bad env in mimick code	barras
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-08-24	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-23	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-07-16	Suppression de Rawterm.loc, branchement sur Util.loc	herbelin
2004-07-13	bug #794: conv made in wrong env	barras
2004-07-13	bug #790: better error_not_clean	barras
2004-07-11	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-06-30	updated printing of evar context (may loop ?)	corbinea
2004-06-29	Essai de suppression de eta dans simpl (cf bug #779)	herbelin
2004-06-28	Double bug d'affichage des cases dépendants (bug #784)	herbelin
2004-06-27	Correction affichage v8 des records avec let (bug #798)	herbelin
2004-06-25	correspondance des records et noms de champs de records entre un module et sa...	letouzey
2004-05-14	test de conversion laissait echapper exception NotConvertible	barras
2004-04-30	Terminologie plus intuitive: evaluable -> unfoldable	herbelin
2004-04-29	Prise en compte d'un type dont la sorte est une evar	herbelin
2004-04-27	Correction incapacité à gérer les annotations de type dépendantes pour le...	herbelin
2004-04-13	Correction confusion entre la dependance en les termes filtrees dans l'annota...	herbelin