aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
2003-04-09Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargsherbelin
2003-04-09Bugs synchronisation pour gestion traduction des implicitesherbelin
2003-04-09Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...herbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-09Prise en compte affichage coercions traducteur dans Constrexternherbelin
2003-04-08Ajout option "Local" à "Open Scope"herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Ajout d'un choix 'onlyparse'herbelin
2003-03-31Restauration de make_all_different (disparu depuis version 1.74) car sinon de...herbelin
2003-03-29Implicit Variables Type dans les inductiveherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-26Ajout de Set Print Widthgregoire
2003-03-13code mortherbelin
2003-03-12*** empty log message ***barras
2003-03-04tous les fichiers passes a Coq IDEfilliatr
2003-03-03fichiers sur la ligne de commande passes a Coq IDEfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:13:02 +0000