coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Add a flush after backtracking x y z and before printing subgoals.	courtieu	2006-10-23
*	Correction de la localisation des erreurs en interactif (numéro de	herbelin	2006-10-20
*	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin	2006-10-09
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin	2006-10-05
*	Added a new option -emacs-U changing emacs prompt delimiters by	courtieu	2006-09-29
*	Corrections mineures	notin	2006-09-25
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin	2006-09-15
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Indentation + svnprop	notin	2006-09-12
*	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin	2006-09-09
*	Finalement, interdiction des points fixes non totalement mutuellement	herbelin	2006-09-06
*	Ajout possibilité clause "where" dans co-points fixes	herbelin	2006-09-01
*	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin	2006-09-01
*	Indentation + typo	notin	2006-09-01
*	improve the amount of information given by the Ltac tactic debugger	bertot	2006-08-28
*	Morceau de code mort	herbelin	2006-08-24
*	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin	2006-07-28
*	Correction du bug #1116	jforest	2006-07-20
*	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin	2006-07-05
*	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin	2006-06-09
*	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin	2006-06-08
*	Réparation coqtop.ml	notin	2006-06-07
*	Changement de l'option -where: on vérifie si la variable d'environnement COQ...	notin	2006-06-07
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	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