aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2003-09-21Renommage Implicits -> Implicitherbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-19parsingherbelin
2003-09-18Plutôt que de faire "Load" silencieusement, en profiter pour traduireherbelin
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
2003-09-16Pour cacher le contenu de Load au traducteurherbelin
2003-09-16Tentative amelioration pretty-printing symbolesherbelin
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...herbelin
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)herbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-12Déplacement d'un morceau de Declareherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
2003-09-12Déplacement de Declare et déclarations des scopes d'argument dans Declareherbelin
2003-09-10Debranchement du traducteur pour Load !herbelin
2003-09-10Traduction de Distfixherbelin
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-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-02Freeze mal placeherbelin
2003-08-31Mise en oeuvre de la syntaxe des inductifs a la ML 'Inductive nat : Set := O ...herbelin
2003-08-14Fusion -translate et -ftranslateherbelin
2003-08-12Bug et amliorations diversesherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-08-11Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsherbelin
2003-08-11Nettoyageherbelin
2003-07-24Bug globalisation Grammar (suite)herbelin
2003-07-23Bug globalisationherbelin
2003-06-23Ajout systématique de Proof dans la traductionherbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-10Distinction mode v7 ou translate; conséquences du déplacement traducteur de...herbelin
2003-06-10Déplacement de code dans command; MAJ DebugOnherbelin
2003-06-10Mise en place structure pour des 'arguments scope' dirigés par une classeherbelin
2003-06-08Tables logarithmiques pour les coercions + nettoyageherbelin
2003-05-23fabrication de ide/utf8.voletouzey
2003-05-23Bug en mode translateherbelin
2003-05-22Ajout V8Notationherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-14coqide: .* on start/add \n on eofmonate
2003-05-13Affichage commentairesherbelin
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-29Moins de ' ' à l'affichageherbelin
2003-04-29Bug fermeture de stdoutherbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
2003-04-10Suppression de quelques espaces superflusherbelin
2003-04-09Formattage affichageherbelin
2003-04-09Correction Show Implicitsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:09:52 +0000