coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-09	error	herbelin
2003-09-02	Export process_module_bindings pour traducteur	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-10	Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...	herbelin
2003-06-10	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin
2003-06-10	code mort	herbelin
2003-05-20	Extension renommage	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-05-19	CoqIde : but reset_mod	filliatr
2003-05-19	configure et make install s'occupent de CoqIde tout seuls	filliatr
2003-05-19	but Require dans une Section	filliatr
2003-05-15	table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...	filliatr
2003-05-14	Deplacement lemmes sur fact de Reals vers Arith	herbelin
2003-05-13	Orthographe anglaise - typos	herbelin
2003-05-13	Orthographe anglaise	herbelin
2003-05-05	Corrige Bug (PR#290)	coq
2003-04-29	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-10	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin
2003-04-09	Bug init_function	herbelin
2003-04-09	Synchronisation séparée des implicites pour l'affichage du traducteur;	herbelin
2003-04-09	Correction Show Implicits	herbelin
2003-04-09	Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs	herbelin
2003-04-09	Synchronisation avec reset	herbelin
2003-04-09	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-04-07	Renommage unicite/unicity pour la v8	herbelin
2003-03-31	Mise en place d'un traducteur de noms v7->v8	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-26	ajout d'une fonction reset_mod	monate
2003-03-13	Ajout réaffichage SubClass	herbelin
2003-03-12	* empty log message *	barras
2003-02-24	False dependencies in summary	coq
2003-02-05	Ajout du traducteur	desmettr
2003-02-03	release 7.4; changement magic number	filliatr
2003-01-31	Pour satisfaire ProofGeneral	coq
2003-01-27	Deux p\'tits trucs ;)	coq
2003-01-22	Bug 'with Module' corrige	coq
2003-01-09	Export M + Module M <: SIG	coq
2002-12-19	Petit netoyage dans lib	coq
2002-12-16	Petit netoyage des open's et commentaires	coq
2002-12-11	Essai de hconsing local au declarations	herbelin
2002-12-10	Hash-consing dès la lib_stk	herbelin
2002-12-09	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq
2002-12-05	des Set et des Map en plus	letouzey
2002-12-04	Correction d'un message d'erreur de l'application de non-foncteur	coq