coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	preparation packages V8.0-cdrom	barras	2004-03-15
*	Bug de Require multiple	herbelin	2004-01-28
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Changement numero magique; message d'erreur en cas de mauvaise syntaxe	herbelin	2003-12-23
*	Reset Initial uniquement interactivement	herbelin	2003-12-19
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	Options -strongly-constructive et -strongly-classical	herbelin	2003-10-28
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Deplacement de iter_constr_with_full_binders dans Termops	herbelin	2003-10-22
*	Nouvelle fonction cherchant tous les noms d'un suffixe donne	herbelin	2003-10-21
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Mise en place d'un mecanisme ne chargeant pas les preuves opaques	herbelin	2003-10-08
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Fonctions utiles	herbelin	2003-09-23
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-23
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	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-12
*	error	herbelin	2003-09-09
*	Export process_module_bindings pour traducteur	herbelin	2003-09-02
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	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-06-10
*	Extension renommage	herbelin	2003-05-20
*	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-19
*	table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...	filliatr	2003-05-15
*	Deplacement lemmes sur fact de Reals vers Arith	herbelin	2003-05-14
*	Orthographe anglaise - typos	herbelin	2003-05-13
*	Orthographe anglaise	herbelin	2003-05-13
*	Corrige Bug (PR#290)	coq	2003-05-05
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin	2003-04-29
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin	2003-04-10
*	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-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Renommage unicite/unicity pour la v8	herbelin	2003-04-07
*	Mise en place d'un traducteur de noms v7->v8	herbelin	2003-03-31
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	ajout d'une fonction reset_mod	monate	2003-03-26
*	Ajout réaffichage SubClass	herbelin	2003-03-13