coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
*	takes better account of the new possibility to pass a parametric count argument	bertot	2004-03-03
*	removes capital letters in two tactic names.	bertot	2004-03-03
*	make sure the implicit argument indications are in the right order	bertot	2004-03-03
*	maj	filliatr	2004-03-03
*	maj	filliatr	2004-03-03
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin	2004-03-02
*	Simplification preuve	herbelin	2004-03-02
*	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