coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ...	notin	2006-05-02
*	Bug assert as	herbelin	2006-05-02
*	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-29
*	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-28
*	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-27
*	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	2006-04-26
*	Prise en compte du Require multiple	herbelin	2006-04-26
*	suite du pont entre Bvector et N	letouzey	2006-04-26
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
*	Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la créat...	notin	2006-04-26
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
*	un lemme de double inclusion	letouzey	2006-04-25
*	Reverting nf_betaiotaevar_preserving_vm_cast	jforest	2006-04-25
*	Code mort (suite)	herbelin	2006-04-25
*	Suppression code mort	herbelin	2006-04-25
*	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin	2006-04-24
*	Changement anomaly en failwith dans out_name pour utilisation par map_succeed	herbelin	2006-04-24
*	Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;	herbelin	2006-04-24
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24