coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-23	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin
2003-10-22	Integration de SearchNamed dans SearchAbout	herbelin
2003-10-22	reorganisation des niveaux (ex: = est a 70)	barras
2003-10-20	bug traduction de auto.(simpl). en auto.simpl.	barras
2003-10-17	Bug des terminaux quotés	herbelin
2003-10-16	oups! ca compile maintenant	barras
2003-10-16	translator avoids printing a . followed by a ( by inserting a space	barras
2003-10-16	Debranchement de l'affichage systematique des projections avec la notation po...	herbelin
2003-10-14	En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...	herbelin
2003-10-14	Changement 'as notation' en 'where notation'	herbelin
2003-10-14	Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...	herbelin
2003-10-13	Admitted rendu independant de Conjecture: plus pratique en mode interactif	herbelin
2003-10-13	Bug introduit dans start_proof par le commit precedent	herbelin
2003-10-13	Petits bugs	herbelin
2003-10-13	Deplacement pr_subgoal and co vers Pfedit	herbelin
2003-10-13	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin
2003-10-13	Protection contre les noms de lemmes existant deja	herbelin
2003-10-13	Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamed	herbelin
2003-10-11	translate_file etait abusivement positionne	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-10-10	Renommage en v8 de PolyList en List et List en MonoList	herbelin
2003-10-09	Nouveau format de l'option 'format'	herbelin
2003-10-08	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin
2003-10-08	Des abbreviations pour constrintern.ml	herbelin
2003-10-08	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin
2003-10-08	Renommage no-strict en -strict-implicit; option -dont-load-proofs	herbelin
2003-10-07	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-10-04	Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)	herbelin
2003-10-03	pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait	herbelin
2003-10-03	Correction bug explosion de la taille de la liste loaded_modules	herbelin
2003-10-01	Implantation de l'option 'format' des Notations	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-26	Ajout 'About'	herbelin
2003-09-26	Decouplage printing en v8 pour les interpretations de notations	herbelin
2003-09-25	V8Infix declarait a tort une regle d'interpretation V7	herbelin
2003-09-24	Traduction aussi si -translate et -load-vernac-source	herbelin
2003-09-23	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin
2003-09-23	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin
2003-09-22	traducteur: affiche les commentaires a l'interieur des commandes	barras
2003-09-22	Anglais	herbelin
2003-09-22	message d'erreur de garde des cofix	barras
2003-09-21	Renommage Implicits -> Implicit	herbelin
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-19	parsing	herbelin
2003-09-18	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin
2003-09-18	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin
2003-09-16	Pour cacher le contenu de Load au traducteur	herbelin
2003-09-16	Tentative amelioration pretty-printing symboles	herbelin