coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tactic Notation et with-names	herbelin	2004-03-02
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02
*	Correction oubli du cas pas d'arguments implicites du tout	herbelin	2004-03-02
*	maj	filliatr	2004-03-02
*	maj	filliatr	2004-03-02
*	ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'	herbelin	2004-03-01
*	code mort	herbelin	2004-03-01
*	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin	2004-03-01
*	Ajout 'replace in'	herbelin	2004-03-01
*	Ajout IntroPattern comme type d'argument générique	herbelin	2004-03-01
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin	2004-03-01
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	Protection d'un 'clear' qui peut etre dependant	herbelin	2004-03-01
*	ocaml 3.07 -> 3.06	filliatr	2004-03-01
*	maj	filliatr	2004-03-01
*	maj	filliatr	2004-03-01
*	Exemple de Frederic	herbelin	2004-02-28
*	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin	2004-02-28
*	MAJ Commentaires	herbelin	2004-02-28
*	Traduction 'Cases' en pattern-matching	herbelin	2004-02-28
*	Eviter la stricte redondance de regles de grammaires v7	herbelin	2004-02-28
*	Prise en compte des implicites au travers des notations et abbreviations	herbelin	2004-02-28
*	maj	filliatr	2004-02-28
*	MAJ	herbelin	2004-02-27
*	Erreur de Bruijn et oubli substitution alias dans annotation du 'match'	herbelin	2004-02-27
*	Ajout test synthese du predicat a partir du cast d'un filtrage avec dependances	herbelin	2004-02-27
*	* empty log message *	filliatr	2004-02-27
*	maj	filliatr	2004-02-27
*	added breakpoints to help ide	corbinea	2004-02-26
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	Not all cases for coercions and locality were handled	bertot	2004-02-26
*	Inclusion des annotations de type des filtrages dans 'Set Printing All'	herbelin	2004-02-26
*	maj	filliatr	2004-02-26
*	indexation Record / bug gallina sur := en V8	filliatr	2004-02-25
*	maj	filliatr	2004-02-25
*	maj	filliatr	2004-02-25
*	coqdoc	filliatr	2004-02-24
*	* empty log message *	filliatr	2004-02-24
*	coqdoc	filliatr	2004-02-24
*	maj	filliatr	2004-02-24
*	Generating of annotations added to Makefile.dir	coq	2004-02-23
*	corrects the treatement of SubClass declarations	bertot	2004-02-23
*	Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...	herbelin	2004-02-21
*	MAJ	herbelin	2004-02-21
*	Export des arguments scope au chargement, pas a l'ouverture (2eme)	herbelin	2004-02-21
*	maj	filliatr	2004-02-21
*	Export des arguments scope au chargement, pas a l'ouverture	herbelin	2004-02-20
*	commit précédent erroné	herbelin	2004-02-20
*	maj	filliatr	2004-02-20