coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	MAJ	herbelin	2006-12-12
*	Test bug #932	herbelin	2006-12-12
*	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin	2006-12-12
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)	herbelin	2006-12-09
*	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin	2006-12-09
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...	filliatr	2006-12-09
*	bug condition de garde	barras	2006-12-08
*	dp	filliatr	2006-12-08
*	contrib/dp	filliatr	2006-12-08
*	Pas d'escamotage des noms rÃ©servÃ©s si Set Printing All actibvÃ©	herbelin	2006-12-08
*	Suite ajout option -output-context	herbelin	2006-12-08
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04...	filliatr	2006-12-08
*	Ajout d'une option -output-context qui affiche le contexte en CCI pur à la	herbelin	2006-12-08
*	Correction typo règle réduction du fix chapitre CCI	herbelin	2006-12-08
*	Subtac bug fix, add list take example.	msozeau	2006-12-08
*	MAJ	herbelin	2006-12-03
*	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin	2006-12-03
*	add a comment about Show Existentials and a question about case_eq	jnarboux	2006-12-01
*	Fork of cases impl for subtac.	msozeau	2006-11-29
*	correction du bug : VM value extraction error (PR#1290)	bgregoir	2006-11-29
*	The $(BEST) binaries symlinks depend on existence of target, not newness.	lmamane	2006-11-27
*	Functional graph merging deals with letins.	courtieu	2006-11-24
*	Fixed the graph merging parameter order.	courtieu	2006-11-24
*	Fixed the -emacs option which was always On.	courtieu	2006-11-24
*	Fixing syntax and parameter order in functional graph merging.	courtieu	2006-11-23
*	Code mort découvert par Matthieu	herbelin	2006-11-22
*	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin	2006-11-21
*	un caractere blanc parasite dans svn:ignore	letouzey	2006-11-21
*	Changing merging functional scheme syntax.	courtieu	2006-11-20
*	Correction boucle du parseur en cas de caractÃère non unicode	herbelin	2006-11-20
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin	2006-11-19
*	mult_sym, plus_sym -> mult_comm, plus_comm	herbelin	2006-11-19
*	MAJ	herbelin	2006-11-19
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Code mort (duplication de code dans reductionops.ml)	herbelin	2006-11-18
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	Small fix in functional graph merging.	courtieu	2006-11-16
*	suppression de code mort (avec bug de nom)	letouzey	2006-11-16
*	pb avec r9379 + modifs dans ring	barras	2006-11-16
*	Work on dep types pattern matching	msozeau	2006-11-16
*	suite de r9362: reconnaissance de qqs injections entre nat, N et Z	barras	2006-11-16
*	Adaptation à FreeBSD	notin	2006-11-16
*	Some usability enhancements.	msozeau	2006-11-15
*	Better solve using tactics impl.	msozeau	2006-11-13
*	Correction de la seconde partie du bug #1278	jforest	2006-11-13
*	Correction de la premiere partie du #1278 (but non referme en cas d'echec)	jforest	2006-11-13
*	Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0	herbelin	2006-11-13