aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2003-02-28Recuperation des outputs de l'interpretation des commandes vernac et des erre...desmettr
2003-02-27Le lexeur et Notation savent reconnaître si un unicode des blocsherbelin
2003-02-13Test de non bouclage malencontreux dans les niveauxherbelin
2003-02-13Chargement dynamique de .cmadelahaye
2003-02-13Debugger plus informatifdelahaye
2003-02-11Undo dans Coq IDEfilliatr
2003-02-05Ajout du traducteurdesmettr
2003-02-04interface GTK2 experimentalemonate
2003-01-31Pour satisfaire ProofGeneralcoq
2003-01-30changement de place du Initial State (maintenant apres l'analyse de la ligne ...filliatr
2003-01-20deplacement du test 'il reste des preuves en cours'filliatr
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2003-01-17msg Failtac; echec -batch s'il reste des preuvesfilliatr
2003-01-16Bugs affichageherbelin
2003-01-16-emacs: plus de prompt entre les lignesfilliatr
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2003-01-09Export M + Module M <: SIGcoq
2003-01-06SearchAboutfilliatr
2002-12-31Amélioration règles d'affichageherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-21Affinement affichageherbelin
2002-12-19Petit netoyage dans libcoq
2002-12-19suite du commit precedentbarras
2002-12-15Prise en compte des scopes traversés dans les notationsherbelin
2002-12-12Ajout du vernac Proof withgregoire
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-09Problèmes et améliorations divers affichageherbelin
2002-12-09Code mort ?herbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-04Modification Require Frommohring
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
2002-12-03Préparation à la prise en compte des changements de scopes internes aux not...herbelin
2002-12-03Pas de globalisation impérative pour les Grammarherbelin
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...herbelin
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
2002-12-02On force l'associativité pour les entrées sans niveauxherbelin
2002-11-29Raffinement syntaxe Infixherbelin
2002-11-28Affinement de la gestion des niveaux toujours; type ETBigintherbelin
2002-11-28typo ?letouzey
2002-11-28Affinement encoreherbelin
2002-11-27Ajout répertoire interpherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 00:17:50 +0000