coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-23	Make sure proof by pointing works.	bertot
2003-01-23	Make proof by pointing work for the new notations of existential quantification.	bertot
2003-01-23	oubli des add_recursors singleton logiques	letouzey
2003-01-23	maj V7.4	letouzey
2003-01-22	MAJ	herbelin
2003-01-22	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot
2003-01-22	petit bug pp haskell	letouzey
2003-01-22	Extraction des modules, enfin !	letouzey
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