coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-20	Ajout erreur GlobalNotFound	herbelin
2000-11-20	Cablage des syntactif defs avec la Nametab des objets	herbelin
2000-11-20	Mieux à sa place dans toplevel	herbelin
2000-11-20	Prise en compte noms longs	herbelin
2000-11-20	Ajout pr_global_reference et is_visible	herbelin
2000-11-20	Tables des eval_constant devient une Cstmap	herbelin
2000-11-20	Une capsule pour save_module_to dans Discharge	herbelin
2000-11-15	mise a jour	filliatr
2000-11-15	Changed the semantics of AddRecPath.	sacerdot
2000-11-15	methode export	filliatr
2000-11-15	-opt ne remplace plus camlp4 par camlp4o.opt car on ne peut pas	filliatr
2000-11-15	concernant les binaires	filliatr
2000-11-13	Retour a la version 1.1	herbelin
2000-11-11	Y avait des '.' non suivis d'un séparateur	herbelin
2000-11-11	Gros hack pour afficher les univers	herbelin
2000-11-11	Code more concernant feu les abstractions	herbelin