coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-20	Petit bug entre close_section's	herbelin
2000-11-20	Mieux à sa place dans toplevel	herbelin
2000-11-20	La variable argument d'un non-terminal dans Grammar est maintenant un Var ( p...	herbelin
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes	herbelin
2000-11-20	Nouveau lexeme METAIDENT pour les $id	herbelin
2000-11-20	Ajout diverses entrées pour les noms qualifiés	herbelin
2000-11-20	Ajout implicits_of_global + accès par noms longs	herbelin
2000-11-20	Tables séparées pour chaque type de global	herbelin
2000-11-20	Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...	herbelin
2000-11-20	Utilisation de global_reference dans rawconstr	herbelin
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes	herbelin
2000-11-20	Prise en compte noms longs	herbelin
2000-11-20	Tables séparées pour chaque type de global; calcul de la Nametab de la sect...	herbelin
2000-11-20	Acceptation des noms qualifiés; utilisation de global_reference dans pattern...	herbelin
2000-11-20	Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...	herbelin
2000-11-20	Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $id	herbelin
2000-11-20	"Distinction entre . suivi d'un blanc et . suivi d'un ident (pour les noms qu...	herbelin
2000-11-20	MAJ	herbelin
2000-11-20	Utilisation de global_reference dans pattern	herbelin