coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-21	Make sure pcoq will also display hypotheses with a value.	bertot
2003-01-21	Add a few operators in the new version of xlate.ml and make sure	bertot
2003-01-20	Utilisation de 'Recursive' pour les tactiques récursives	herbelin
2003-01-19	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-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-09	Export M + Module M <: SIG	coq
2003-01-06	SearchAbout	filliatr
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	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-18	stupide inlining des construsteurs	letouzey
2002-12-15	Ajout "Locate Notation"	herbelin
2002-12-15	Evaluation paresseuse de l'affichage du debug	herbelin
2002-12-13	debut de parcours des modules	letouzey
2002-12-13	une branche de case inutile	letouzey
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-11	Compensation de suppression betaiota de type_of	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-10	Normalisation des types (fait avant dans Typing)	herbelin
2002-12-09	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-05	reorganisation des recherches de ref dans ml_decl	letouzey
2002-12-05	code cleanup (+ debut de commencement de modules)	letouzey
2002-12-04	Modification Require From	mohring
2002-12-03	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-02	Remplacement Grammar par Notation	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-11-29	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-28	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-27	Extraction des Record, suite	letouzey
2002-11-26	Remplacement Grammar/Syntax par Notation	herbelin