aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-02-05majfilliatr
2004-02-04Reconnaissance précoce de la dépendance du prédicat en un terme filtréherbelin
2004-02-04Vérification de la prise en compte des termes de type non inductifherbelin
2004-02-04clean-ide plus precisherbelin
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...herbelin
2004-02-04Boite autour des quote pour eviter un retour a la ligne apres le premier guil...herbelin
2004-02-04bug fix find coqidecoq
2004-02-04highlightmarche
2004-02-04search windowcoq
2004-02-04majfilliatr
2004-02-03MAJherbelin
2004-02-03Relachement condition pour afficher @ en cas d'explicitation d'implicitesherbelin
2004-02-03Relachement condition pour declarer un inductif dans la table des 'If'; contr...herbelin
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ...herbelin
2004-02-03Bug focusherbelin
2004-02-03Protection contre noms de variable indefinis et guillemets autour des constrherbelin
2004-02-03Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un no...herbelin
2004-02-03majfilliatr
2004-02-02reorganize the order of librairies in the entry CMO to make sure this canbertot
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
2004-01-31majfilliatr
2004-01-30updates the definition of tactics using Ltac and adds the subst tacticbertot
2004-01-30adds module commands and update the extration commandbertot
2004-01-30majfilliatr
2004-01-30majfilliatr
2004-01-29pour win32coq
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...herbelin
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant que...herbelin
2004-01-29pour ide sous windowscoq
2004-01-29MAJherbelin
2004-01-29Suppression de 'Print.' en v8herbelin
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...herbelin
2004-01-29updates the tactics contradiction and autorewrite, the commandsbertot
2004-01-29majfilliatr
2004-01-28Bug de Require multipleherbelin
2004-01-28make sure that 'in' clauses for reduction tactics are translatedbertot
2004-01-28majfilliatr
2004-01-28majfilliatr
2004-01-27Bug activation erronée du traducteur en v8herbelin
2004-01-27meilleure separation de compil et install de coq, coqide et coq-interfacebarras
2004-01-27Correction des cibles des theories indviduellesherbelin
2004-01-27MAJ simplificationherbelin
2004-01-27Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...herbelin
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...herbelin
2004-01-27majfilliatr
2004-01-27majfilliatr
2004-01-26deplacement des cma et cmxa dans les sous-repertoiresbarras
2004-01-26reparation de qqs bugs du traducteurbarras
2004-01-26a try to make intro patterns betterbertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 18:21:22 +0000