coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	bug traduction de auto.(simpl). en auto.simpl.	barras	2003-10-20
*	Bug des terminaux quotés	herbelin	2003-10-17
*	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-16
*	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-14
*	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-13
*	translate_file etait abusivement positionne	herbelin	2003-10-11
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Nouveau format de l'option 'format'	herbelin	2003-10-09
*	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-08
*	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-07
*	Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)	herbelin	2003-10-04
*	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-03
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Ajout 'About'	herbelin	2003-09-26
*	Decouplage printing en v8 pour les interpretations de notations	herbelin	2003-09-26
*	V8Infix declarait a tort une regle d'interpretation V7	herbelin	2003-09-25
*	Traduction aussi si -translate et -load-vernac-source	herbelin	2003-09-24
*	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-23
*	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-22
*	Renommage Implicits -> Implicit	herbelin	2003-09-21
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	parsing	herbelin	2003-09-19
*	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-18
*	Pour cacher le contenu de Load au traducteur	herbelin	2003-09-16
*	Tentative amelioration pretty-printing symboles	herbelin	2003-09-16
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...	herbelin	2003-09-16
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)	herbelin	2003-09-16
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12