aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-09-03option pour supprimer les menus contextuels sur les butsmarche
2003-09-03Projectionsherbelin
2003-09-03*** empty log message ***herbelin
2003-09-03majfilliatr
2003-09-02Relachement conflit 'with' dans le cas des Module with Definitionherbelin
2003-09-02Contorsions pour que l'interpretation deses foncteurs depende des parametres ...herbelin
2003-09-02Freeze mal placeherbelin
2003-09-02Export process_module_bindings pour traducteurherbelin
2003-09-02auto completion disabled par defautmarche
2003-09-02Bug traduction Search, SearchPattern, etc.herbelin
2003-09-02Plus de passage du scope tmp sous les lambdasherbelin
2003-09-01Passage de 'relation' à Typeherbelin
2003-09-01majfilliatr
2003-08-31Syntaxe des constructeurs et des hypothesesherbelin
2003-08-31Bug et améliorations diversherbelin
2003-08-31'Assumptions' sur le modèle général des lieursherbelin
2003-08-31Symetrisation des changements implicites de scopeherbelin
2003-08-31Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...herbelin
2003-08-31Affichage des inductifs en v8herbelin
2003-08-31V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclassherbelin
2003-08-28correction d'un stack overflow possible (PR#320)letouzey
2003-08-15majfilliatr
2003-08-14Fusion -translate et -ftranslateherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 03:29:41 +0000