coq - The formal proof system

Age	Commit message (Expand)	Author
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-02	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-01	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-02-28	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-27	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-26	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-25	indexation Record / bug gallina sur := en V8	filliatr
2004-02-25	maj	filliatr
2004-02-25	maj	filliatr
2004-02-24	coqdoc	filliatr
2004-02-24	* empty log message *	filliatr
2004-02-24	coqdoc	filliatr
2004-02-24	maj	filliatr