aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2002-12-19Petit netoyage dans libcoq
2002-12-19suppression de l'archive cvs d'un bout de debugletouzey
2002-12-19les empty ind et les singletons etaient oublies par add_recursorsletouzey
2002-12-19simplification de solve_subgoal: n'utilise plus frontierbarras
2002-12-18stupide inlining des construsteursletouzey
2002-12-15Ajout "Locate Notation"herbelin
2002-12-15Evaluation paresseuse de l'affichage du debugherbelin
2002-12-13debut de parcours des modulesletouzey
2002-12-13une branche de case inutileletouzey
2002-12-12Ajout du vernac Proof withgregoire
2002-12-11Compensation de suppression betaiota de type_ofherbelin
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-10Normalisation des types (fait avant dans Typing)herbelin
2002-12-09Ajoute le bon traitement pour Ring, Locate, Commentsbertot
2002-12-09Take notations into account: numbers and the CNotation operator.bertot
2002-12-09Problèmes et améliorations divers affichageherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-12-09ppletouzey
2002-12-09petit bugletouzey
2002-12-09chamboulement du codage des indcutifs extraits; deplacements des tables; ...letouzey
2002-12-05reorganisation des recherches de ref dans ml_declletouzey
2002-12-05code cleanup (+ debut de commencement de modules)letouzey
2002-12-04Modification Require Frommohring
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
2002-12-03Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvellesbertot
2002-12-02Remplacement Grammar par Notationherbelin
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
2002-11-292 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversletouzey
2002-11-29Raffinement syntaxe Infixherbelin
2002-11-29cosmetiqueletouzey
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
2002-11-28Court-circuit de g_zsyntaxherbelin
2002-11-28suite et fin des records avec ocamlletouzey
2002-11-28 bug pp letin + un inductif constant n'est pas un recordletouzey
2002-11-28Re-Oupsletouzey
2002-11-28Oupsletouzey
2002-11-28Reorganisation du pretty-print:letouzey
2002-11-28Nettoyageherbelin
2002-11-27Extraction des Record, suiteletouzey
2002-11-26Remplacement Grammar/Syntax par Notationherbelin
2002-11-26Remplacement des Grammar et des [| |] par des notationsherbelin
2002-11-26debut de support des records camlletouzey
2002-11-25correction bug n°191letouzey
2002-11-25cleanup table.ml + erreur si Extraction Inline sous sectionletouzey
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-11-24Nettoyageherbelin
2002-11-18remaniement de test_extraction.vletouzey
2002-11-18typoherbelin
2002-11-16Complétion du commit précédentherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 22:50:36 +0000