aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2004-01-26majfilliatr
2004-01-26majfilliatr
2004-01-24streamlines the keywords for definitions, require commandsbinders, notationbertot
2004-01-24majfilliatr
2004-01-23MAJherbelin
2004-01-23Bug induction lors de types inductives avec parametresherbelin
2004-01-23majfilliatr
2004-01-22change add path commands to get the extra argument and the Hint commandsbertot
2004-01-22Correction lecture des locations si pas demandees dans l'ordreherbelin
2004-01-22Protection table des locations lors de Load (pour coqdoc)herbelin
2004-01-22fixes argument lists for tactic definitions, updates inversion tacticsbertot
2004-01-22adds a clause argument to symmetrybertot
2004-01-22corrects the way the structural argument declaration is handled inbertot
2004-01-22adds the notations in inductive definitions, improves the consistency betweenbertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:43:49 +0000