coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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-21
*	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-20
*	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-15