aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...herbelin
2000-07-20portage Refinefilliatr
2000-07-04correctionmayero
2000-07-03ajoutsmayero
2000-07-03Traduction de syntaxe vers ltacdelahaye
2000-07-01Séparation des caractères spéciaux par un blancherbelin
2000-07-01Retrait des parenthèses inutiles autour des tactiquesherbelin
2000-06-21Require Plus ajoutefilliatr
2000-06-21theories/Realsfilliatr
2000-06-21theories/Relationsfilliatr
2000-06-21theories/Setsfilliatr
2000-06-21theories/Listsfilliatr
2000-05-22Séparation des tokens -> et ~herbelin
2000-05-22Changement nommage des hypothèses; parenthèses pour les tactiquesherbelin
2000-05-22Parenthèsesherbelin
2000-05-18parethèses de tactiquesherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-05-02portage Omega (mais toujours pas Zpower et Zlogarithm)filliatr
2000-04-30Bug affichage Error et Valueherbelin
2000-04-26suppression doublonfilliatr
2000-03-30erreurs lexicales dans les patterns (manquait des espaces)filliatr
2000-03-21 - bug make_module_marker (plus de # et de .obj maintenant)filliatr
2000-03-21Retour sur les anciens nomsherbelin
2000-03-21Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...herbelin
2000-03-18Zarithfilliatr
2000-03-18g_natsyntax.mlfilliatr
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
2000-03-16mise sous CVSfilliatr
2000-03-10t -> $t dans regle grammaire EXfilliatr
2000-03-10mise sous CVS du repertoire theories/Arithfilliatr
2000-03-10*** empty log message ***barras
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
2000-01-07Renommage command en constrherbelin
1999-12-16erreurs de syntax :$filliatr
1999-12-13 - méthode load sur les Hintsfilliatr
1999-12-13fichiers prelude Coqfilliatr