coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-20	Ajout sp_of_global; Introduction constant_path = section_path	herbelin
2000-11-20	Prise en compte camlp4.opt dans la configuration et le Makefile	herbelin
2000-11-20	Utilisation de global_reference dans rawconstr	herbelin
2000-11-20	Utilisation de global_reference dans rawconstr; blindage pour quand appelé d...	herbelin
2000-11-20	Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...	herbelin
2000-11-20	Introduction constant_path = section_path	herbelin
2000-11-20	Open est maintenant géré par Nametab	herbelin
2000-11-20	Nouveaux points d'accès pour les noms qualifiés	herbelin
2000-11-20	Bug dans la règle de syntaxe de ex2	herbelin
2000-11-20	Nouvelle structure arborescente à la Nametab pour prendre en compte les noms...	herbelin
2000-11-20	Prise en compte constructeur QUALID pour noms qualifiés	herbelin
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ...	herbelin
2000-11-20	Nettoyage + prise en compte noms longs	herbelin
2000-11-20	Suppression de la section fast_integer qui cachait le nom du module éponyme	herbelin
2000-11-20	Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique export...	herbelin