coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-19	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
2008-05-01	Clarification de l'ordre d'interprétation des variables dans ltac. En	herbelin
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2007-02-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-09-22	Test Tactic Notation	herbelin
2006-03-05	Ajout test relatif au bug #984	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-02-02	test de la bonne position des vars de ltac entre les vars et les rels	herbelin
2004-09-25	Ajouts	herbelin
2004-03-11	Ajout exemple Inst	herbelin
2003-05-22	Test backtracking	herbelin
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2002-06-14	* empty log message *	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context	herbelin
2001-12-21	* empty log message *	herbelin