coq - The formal proof system

Age	Commit message (Expand)	Author
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	Prise en compte des noms qualifiés dans certaines commandes	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	Utilisation de global_reference dans pattern	herbelin
2000-11-20	Utilisation de global_reference dans rawconstr	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	Ajout pr_global_reference et is_visible	herbelin
2000-11-09	Amélioration message d'erreur arg explicité au lieu d'arg normal	herbelin
2000-11-08	nouveau load path	filliatr
2000-11-08	out_variable (Liboject.obj -> ...) distibgue de get_variable	filliatr
2000-11-07	MAJ	herbelin
2000-11-07	Changement/extension dans les noms de parseurs de Grammar	herbelin
2000-11-06	Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...	herbelin
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-11-05	Nouveau mode de compilation de .ml4	herbelin
2000-11-05	Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...	herbelin
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-31	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr
2000-10-30	Priorite du Try/Orelse + Debug switch + correction bug dans Pattern	delahaye
2000-10-26	Renommage var en named et decl en assum	herbelin
2000-10-24	Bug de copier-coller	herbelin
2000-10-21	Pb affichage warning	herbelin
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-10-18	Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...	herbelin
2000-10-18	2ème	herbelin
2000-10-18	Mise en place de parseurs avec globalisation pas seulement dans les quotation...	herbelin
2000-10-18	Nettoyage	herbelin
2000-10-18	globalize_command devient globalize_constr	herbelin
2000-10-18	Correction pb de globalisation dans print_mutual	herbelin
2000-10-17	Pb factorisation de Print Grammar	herbelin
2000-10-16	Changement "command" en "constr" et globalize_command en globalize_constr	herbelin
2000-10-11	Suite du précédent	herbelin
2000-10-10	Plus d'échec sur les globaux lorsque prterm est appelé par le débugger	herbelin
2000-10-06	Correction incompatibilites dans la fn des types des inductifs	herbelin
2000-10-05	Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALIST	herbelin
2000-10-04	Utilisation de local_strong plutôt que strong buggé avec défs locales	herbelin
2000-10-03	Ajout castedopenconstrarg	herbelin
2000-10-03	Ajout de globpr dans tacpr	herbelin
2000-10-03	Ajout castedopenconstrarg; Renommage tactique Let en LetTac	herbelin
2000-10-03	Reorganisation des interp_constr	herbelin
2000-10-01	Renommage AppL en App	herbelin
2000-10-01	Disparition du type oper mais nouveau type global_reference	herbelin