coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest	2006-05-03
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Modification of emacs output: No more show script at the end of a proof.	courtieu	2006-04-27
*	Modification of emacs output: Pp.warning and al now output warning	courtieu	2006-04-27
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	Modification of "Show Intros": it now shows letins too.	courtieu	2006-04-11
*	Finalement, scopes utiles pour option 'where' (cf bug #1132)	herbelin	2006-04-07
*	Suppression du test Proof with <tac>	notin	2006-04-05
*	- correction du bug #1055	notin	2006-03-27
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Correction du bug 808: il est maintenant interdit de déclarer une assomption...	coq	2006-03-02
*	Bug correction in saving proofs: If a hook opens a proof but does not close i...	bertot	2006-02-13
*	Messages nth branche	herbelin	2006-02-07
*	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin	2006-02-07
*	warning seulement si mode verbose	herbelin	2006-02-06
*	Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la	herbelin	2006-01-30
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin	2006-01-28
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	* empty log message *	coq	2006-01-16
*	Correction dans vernac_exact_proof -- jmn	coq	2006-01-16
*	Correction du bug #1055	coq	2006-01-13
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Prise en compte de notations numérales définies au niveau utilisateur+ lég...	herbelin	2006-01-08
*	Réorganisation; suppression code mort; documentation	herbelin	2006-01-07
*	Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...	herbelin	2006-01-04
*	Mini-restructuration	herbelin	2005-12-30
*	Autres suppressions de composantes du traducteur	herbelin	2005-12-27
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Changement de stratégie vis à vis du positionnement du module Top en mode b...	herbelin	2005-12-24
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Correction printer des Tactic Notation	herbelin	2005-12-23
*	option '-top dir' now works also in batch mode (2ème)	herbelin	2005-12-22
*	option '-top dir' now works also in batch mode; it is even necessary to ensur...	herbelin	2005-12-22
*	Double bug de interp_modifiers anciennement caché par un troisième que les ...	herbelin	2005-12-22
*	Divers; restructuration des points d'entrée de Constrintern	herbelin	2005-12-21
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin	2005-12-20
*	Suppression de la mise en boite automatique si format utilisateur	herbelin	2005-12-19
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Orthographe de 'instantiate'	herbelin	2005-12-17
*	Changement des named_context	gregoire	2005-12-02
*	bug de coqide sous windows (bad file descriptor)	barras	2005-11-23
*	bug #909: Top n'est cree que si le contexte est vide	barras	2005-11-23
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	- debugging og "Show Intros": no line breaking + fresh ids	coq	2005-11-08
*	Point-virgule manquant ligne 914 détecté par nouveau warning X de ocaml 3.09	herbelin	2005-11-04