coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	Simplification de Simplify (plus de ())	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin	2003-01-15
*	Export M + Module M <: SIG	coq	2003-01-09
*	SearchAbout	filliatr	2003-01-06
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Petit netoyage dans lib	coq	2002-12-19
*	suppression de l'archive cvs d'un bout de debug	letouzey	2002-12-19
*	les empty ind et les singletons etaient oublies par add_recursors	letouzey	2002-12-19
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	stupide inlining des construsteurs	letouzey	2002-12-18
*	Ajout "Locate Notation"	herbelin	2002-12-15
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	debut de parcours des modules	letouzey	2002-12-13
*	une branche de case inutile	letouzey	2002-12-13
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
*	Normalisation des types (fait avant dans Typing)	herbelin	2002-12-10
*	Ajoute le bon traitement pour Ring, Locate, Comments	bertot	2002-12-09
*	Take notations into account: numbers and the CNotation operator.	bertot	2002-12-09
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	pp	letouzey	2002-12-09
*	petit bug	letouzey	2002-12-09
*	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey	2002-12-09
*	reorganisation des recherches de ref dans ml_decl	letouzey	2002-12-05
*	code cleanup (+ debut de commencement de modules)	letouzey	2002-12-05
*	Modification Require From	mohring	2002-12-04
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot	2002-12-03
*	Remplacement Grammar par Notation	herbelin	2002-12-02
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'envers	letouzey	2002-11-29
*	Raffinement syntaxe Infix	herbelin	2002-11-29
*	cosmetique	letouzey	2002-11-29
*	Remaniement du pp, suite: vers un renommage modulaire correcte	letouzey	2002-11-28
*	Court-circuit de g_zsyntax	herbelin	2002-11-28
*	suite et fin des records avec ocaml	letouzey	2002-11-28
*	bug pp letin + un inductif constant n'est pas un record	letouzey	2002-11-28
*	Re-Oups	letouzey	2002-11-28
*	Oups	letouzey	2002-11-28
*	Reorganisation du pretty-print:	letouzey	2002-11-28
*	Nettoyage	herbelin	2002-11-28
*	Extraction des Record, suite	letouzey	2002-11-27
*	Remplacement Grammar/Syntax par Notation	herbelin	2002-11-26
*	Remplacement des Grammar et des [\| \|] par des notations	herbelin	2002-11-26
*	debut de support des records caml	letouzey	2002-11-26