coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-25	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-24	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-20	decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)	letouzey
2006-04-16	Nouveau mécanisme pour les modules interactifs : les arguments de	herbelin
2006-04-16	Added code to support "Program Lemma/Example... etc"	msozeau
2006-04-15	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin
2006-04-15	Tests notations	herbelin
2006-04-15	Test synchronisation chargement objets non logiques	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-14	Pas fier	herbelin
2006-04-14	mise a jour credits	cpaulin
2006-04-14	Enleve les commentaires	cpaulin
2006-04-14	Test files for subtac.	msozeau