coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin
2006-01-21	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin
2006-01-16	* empty log message *	coq
2006-01-16	Correction dans vernac_exact_proof -- jmn	coq
2006-01-13	Correction du bug #1055	coq
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2006-01-08	Prise en compte de notations numérales définies au niveau utilisateur+ lég...	herbelin
2006-01-07	Réorganisation; suppression code mort; documentation	herbelin
2006-01-04	Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...	herbelin
2005-12-30	Mini-restructuration	herbelin
2005-12-27	Autres suppressions de composantes du traducteur	herbelin
2005-12-26	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-24	Changement de stratégie vis à vis du positionnement du module Top en mode b...	herbelin
2005-12-23	Simplifification de vernac_expr li l'abandon du traducteur	herbelin
2005-12-23	Correction printer des Tactic Notation	herbelin
2005-12-22	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-21	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-20	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin
2005-12-19	Suppression de la mise en boite automatique si format utilisateur	herbelin
2005-12-17	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