coq - The formal proof system

Age	Commit message (Expand)	Author
2006-11-17	The emacs-U option now does not output any char above 250.	courtieu
2006-11-02	gestion speciale du niveau 5 des ltac	barras
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-28	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin
2006-10-28	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin
2006-10-23	bug #1194: normalisation evars a la sortie de focus	barras
2006-10-23	Add a flush after backtracking x y z and before printing subgoals.	courtieu
2006-10-20	Correction de la localisation des erreurs en interactif (numéro de	herbelin
2006-10-09	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin
2006-10-05	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin
2006-09-29	Added a new option -emacs-U changing emacs prompt delimiters by	courtieu
2006-09-25	Corrections mineures	notin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-15	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-12	Indentation + svnprop	notin
2006-09-09	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin
2006-09-06	Finalement, interdiction des points fixes non totalement mutuellement	herbelin
2006-09-01	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-08-28	improve the amount of information given by the Ltac tactic debugger	bertot
2006-08-24	Morceau de code mort	herbelin
2006-07-28	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin
2006-07-20	Correction du bug #1116	jforest
2006-07-05	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin
2006-06-09	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin
2006-06-08	Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...	notin
2006-06-07	Réparation coqtop.ml	notin
2006-06-07	Changement de l'option -where: on vérifie si la variable d'environnement COQ...	notin
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	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-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-11	Modification of "Show Intros": it now shows letins too.	courtieu
2006-04-07	Finalement, scopes utiles pour option 'where' (cf bug #1132)	herbelin
2006-04-05	Suppression du test Proof with <tac>	notin
2006-03-27	- correction du bug #1055	notin
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-03-02	Correction du bug 808: il est maintenant interdit de déclarer une assomption...	coq
2006-02-13	Bug correction in saving proofs: If a hook opens a proof but does not close i...	bertot
2006-02-07	Messages nth branche	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-02-06	warning seulement si mode verbose	herbelin
2006-01-30	Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la	herbelin
2006-01-28	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin