aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-08-14Traducteur de correctnessherbelin
2003-08-14code mortherbelin
2003-08-14Traduction mlnamesherbelin
2003-08-14Pb de mot-cleherbelin
2003-08-14Amélioration affichage syntaxe modulesherbelin
2003-08-14Positionnement precoce de l'option -v7herbelin
2003-08-14Ajout token '!' pour correctnessherbelin
2003-08-14Enregistrement tuple_constrherbelin
2003-08-14Notation access au dessous du niveau applicatif (2eme)herbelin
2003-08-13Hack pour ajouter Proof apres Correctnessherbelin
2003-08-13Notation access au dessous du niveau applicatifherbelin
2003-08-12Bug et améliorations diversesherbelin
2003-08-12Bug et amliorations diversesherbelin
2003-08-12Bug détypage du fixherbelin
2003-08-12majfilliatr
2003-08-11Ajout LetTupleherbelin
2003-08-11Mémo nouvelle syntaxeherbelin
2003-08-11MAJherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-08-11Option -v8 à coqtop lance coqtopnewherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin