coq - The formal proof system

Age	Commit message (Expand)	Author
2000-11-24	resolution implicites dans produits (bug)	filliatr
2000-11-24	SearchPattern et SearchRewrite	filliatr
2000-11-24	MAJ	herbelin
2000-11-24	synchronisation Require	filliatr
2000-11-24	- coqc: utilise le meilleur coq possible	filliatr
2000-11-24	Petite simplif due au nouveau Tauto	delahaye
2000-11-24	Nouveau choix pour l'intros initial	delahaye
2000-11-23	Ajout d'une syntaxe pour Reals.	mayero
2000-11-23	On n'introduit que des produits non dependants	delahaye
2000-11-23	Correction d'un bug lorsque des Variables sont clearees dans le but courant	delahaye
2000-11-23	Affichage des QUALID	herbelin
2000-11-23	Simplification de l'accès aux globaux	herbelin
2000-11-23	Search réparé	filliatr
2000-11-23	MAJ	herbelin
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp	herbelin
2000-11-23	id_of_global devient sp_of_global	herbelin
2000-11-23	Fonction qualid_of_global pour affichage des paths avec des '.'	herbelin
2000-11-23	Affichage des paths avec des '.', 2eme; prise en compte qualid	herbelin
2000-11-23	Informations inutiles	herbelin
2000-11-23	Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;	herbelin
2000-11-23	print_id, print_sp -> pr_id, pr_sp	herbelin
2000-11-23	Ajout push_rels_assum	herbelin
2000-11-23	Bug qualidconstarg (intervient pour Transparent)	herbelin
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-22	Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...	herbelin
2000-11-22	Nettoyage	herbelin
2000-11-22	deplacement poly_args; iterateurs sur les segments	filliatr
2000-11-22	Reparation bug mutuels ind	mohring
2000-11-22	retablissement de line_oriented_parser pour Yves	filliatr
2000-11-22	des proofs/macros qui trainaient dans le Makefile et le .depend	filliatr
2000-11-21	Tout est deja traite dans Tacinterp	delahaye
2000-11-21	Elimination d'un test sur les macros	delahaye
2000-11-21	Traitement du pretty-print des Redexp	delahaye
2000-11-21	Ajout d'une fonction pour recuperer la liste des constantes	delahaye
2000-11-21	Ajout du clean pour tolink.ml	delahaye
2000-11-21	reset_name: try / with juste autour de find_entry_p (=> propage les	filliatr
2000-11-21	ln -sf au lieu de ln -s	filliatr
2000-11-21	ajout d'un frozen_state après la fermeture d'une section (sinon bug !)	filliatr
2000-11-21	implicites manuels	filliatr
2000-11-21	PatternMatchingFailure n'etait pas rattrapee	herbelin
2000-11-21	Nettoyage	herbelin
2000-11-21	Bugs make_tuple et existS_pattern	herbelin
2000-11-21	MAJ	herbelin
2000-11-21	ajout de theories/Wellfounded	filliatr
2000-11-21	Begin-End Silent deviennent Set?Unset Silent	mohring
2000-11-21	correction bug Reset	filliatr
2000-11-21	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr
2000-11-21	XML débranché	filliatr
2000-11-21	Prise en compte des implicites dans les regles de grammaires	herbelin