coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Clarification de l'ordre d'interprétation des variables dans ltac. En	herbelin	2008-05-01
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Réparation absence d'interprétation des liaisons vers listes	herbelin	2007-02-15
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin	2006-10-25
*	Test Tactic Notation	herbelin	2006-09-22
*	Ajout test relatif au bug #984	herbelin	2006-03-05
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-21
*	test de la bonne position des vars de ltac entre les vars et les rels	herbelin	2005-02-02
*	Ajouts	herbelin	2004-09-25
*	Ajout exemple Inst	herbelin	2004-03-11
*	Test backtracking	herbelin	2003-05-22
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
*	* empty log message *	herbelin	2002-06-14
*	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	2002-06-13
*	* empty log message *	herbelin	2001-12-21