aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-09-10Passage des projections au niveau 1herbelin
2003-09-109 est associatif a gaucheherbelin
2003-09-10Debranchement du traducteur pour Load !herbelin
2003-09-10warning vers std_errherbelin
2003-09-10Bug predicat old Caseherbelin
2003-09-10Traduction de Distfixherbelin
2003-09-10typonarboux
2003-09-10Ajout 'mod' comme keywordherbelin
2003-09-10Oubli des guillemets dans Commentsherbelin
2003-09-10Pretty-pretting fixherbelin
2003-09-10majfilliatr
2003-09-09Bug predicat let-tupleherbelin
2003-09-09MAJherbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-09Traduction des réferences arguments de commandes non primitives; 'Grammar ta...herbelin
2003-09-09'Grammar tactic' devient 'Tactic Notation'herbelin
2003-09-09Ajout If; synchro avec constrexternherbelin
2003-09-09Ajout If; renommage de l'ident '_'herbelin
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
2003-09-09Ajout If; protection contre clash dans return_typeherbelin
2003-09-09Code mortherbelin
2003-09-09errorherbelin
2003-09-09Protection traducteur contre meta de Grammar tacticherbelin
2003-09-08majfilliatr
2003-09-06MAJherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Check local definitions in context of inductive typesherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-09-06'Implicits qid' -> 'Implicit Arguments qid'herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-06cosmetiqueherbelin
2003-09-06Adapter l'entree de grammaire a la version 7 ou 8herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-06Pour accomoder autant le printer v8 que v7herbelin
2003-09-06Protection contre les types sans corps associéherbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
2003-09-05principes de récurrences plus efficaces pour l'extractionletouzey
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
2003-09-05Zabs_Zsgnletouzey
2003-09-05highlighting de Extractionletouzey
2003-09-05bug dans calcul nb d'occurrencesletouzey
2003-09-05affichage de la nature des colonnesfilliatr
2003-09-05install coqwcfilliatr
2003-09-05coqwcfilliatr
2003-09-05Impression sans ',' des constructeurs de meme type, pour v8herbelin
2003-09-03Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:56:18 +0000