coq - The formal proof system

Age	Commit message (Expand)	Author
2006-05-05	Correction comportement clause _ du match goal	herbelin
2006-05-05	un Zgcd general gardant trace des coefs	letouzey
2006-05-05	encore un correctif sur le rewrite H in setoid:	letouzey
2006-05-04	- intégration de la modification suggérée par L. Mamane: coqmktop passe ma...	notin
2006-05-03	Fixing two minor bugs in recdef and graph of function generation.	jforest
2006-05-03	fixed bug #804: removed useless reduction in fix guard checking	barras
2006-05-03	bug #1096: whd_stack on one arg of conversion had side-effect on the other arg	barras
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-05-02	Changement de comportement de rewrite: face a une egalité setoid, on	letouzey
2006-05-02	Correction bug du correctif bug assert as	herbelin
2006-05-02	Option --coqlib_path pour coqdoc (suite et fin)	notin
2006-05-02	Affichage des warning gtk comme warning coq	herbelin
2006-05-02	Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ...	notin
2006-05-02	Bug assert as	herbelin
2006-04-29	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey
2006-04-29	meilleur nommage pour PairOrderedType	letouzey
2006-04-29	qq proprietes de plus sur Ncompare	letouzey
2006-04-28	Continue l'écriture de la doc de "Function". Pas fini, manque:	courtieu
2006-04-28	If function creates proof obligation, there are now printed once.	courtieu
2006-04-28	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8767 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8766 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8765 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8764 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8763 85f007b7-540e-04...	notin
2006-04-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8762 85f007b7-540e-04...	notin
2006-04-28	Ajout bug #1102	herbelin
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-28	Typo dans précédent commit (8755); protection renforcée dans analyse claus...	herbelin
2006-04-27	MAJ	herbelin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-27	Message d'erreur plus informatif	herbelin
2006-04-27	Official MoWGLI definition of CIC dtd	herbelin
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	Suppression de l'entrée devdoc dans le Makefile principal et modification en...	notin
2006-04-27	Ajout de la doc de l'option -stdout de coqdoc	notin
2006-04-27	Modification of emacs output: Pp.warning and al now output warning	courtieu
2006-04-27	Modification of emacs output: Pp.warning and al now output warning	courtieu
2006-04-27	préparation de add_glob en vue d'isolement de la partie module pour	herbelin
2006-04-27	Ajout chop_dirpath	herbelin
2006-04-27	2-3 lemmes en plus pour que les Bvectors soient effectivement utilisables	letouzey
2006-04-27	Added a short doc for "Function". To be finished.	courtieu
2006-04-26	MAJ	herbelin
2006-04-26	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin
2006-04-26	Outil de test de la réversibilité du réafficheur v8->v8	herbelin
2006-04-26	Diverses corrections de l'afficheur et du traducteur pour s'assurer de	herbelin
2006-04-26	Régénération après mise à jour coqdep pour traiter Require multiple	herbelin