aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Prise en compte `?' dans les `` ``Gravatar herbelin2000-12-06
* Reparation d'un bug de pretty-printGravatar delahaye2000-12-05
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Elimination du 'Gravatar delahaye2000-11-28
* Remettre une section dans fast_integer pour contourner un bug de définition ...Gravatar herbelin2000-11-27
* La bonne modif des UnfoldGravatar herbelin2000-11-27
* Suppression de Unfold inutile et maintenant échouantGravatar herbelin2000-11-27
* Changement du parseur par défaut dans SyntaxGravatar herbelin2000-11-27
* Le nouvel Induction s'appelle NewInductionGravatar herbelin2000-11-26
* Petite simplif due au nouveau TautoGravatar delahaye2000-11-24
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* NettoyageGravatar herbelin2000-11-21
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Bug dans la règle de syntaxe de ex2Gravatar herbelin2000-11-20
* Nettoyage + prise en compte noms longsGravatar herbelin2000-11-20
* Suppression de la section fast_integer qui cachait le nom du module éponymeGravatar herbelin2000-11-20
* Retour a la version 1.1Gravatar herbelin2000-11-13
* Y avait des '.' non suivis d'un séparateurGravatar herbelin2000-11-11
* mise-a-jour, ajouts de quelques truc...Gravatar mayero2000-11-10
* Finalement PolyListSyntax est necessaire (la redondance venait d'une confusio...Gravatar herbelin2000-11-10
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* OrthographeGravatar herbelin2000-11-07
* Plus besoin de débrancher la preuve qui ne passait pasGravatar herbelin2000-11-05
* Plus besoin de rajouter "Require Plus"Gravatar herbelin2000-11-05
* Pour ne plus éviter temporairement le "Auto with zarith" !Gravatar herbelin2000-11-05
* Suppression d'Intuition (trop intelligent?)Gravatar delahaye2000-10-30
* Pour eviter temporairement le "Auto with zarith"Gravatar delahaye2000-10-30
* Passage command -> constrGravatar herbelin2000-10-27
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
* Mise a jour TheoryListGravatar mohring2000-10-27
* Retire les parentheses autour des tactiquesGravatar mohring2000-10-26
* Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...Gravatar herbelin2000-10-18
* ParenthesesGravatar herbelin2000-10-12
* Finalement, encore un Simpl inutileGravatar herbelin2000-10-10
* Parenthèses pour les tactiquesGravatar herbelin2000-10-06
* Changement dans la stratégie de réduction du Fix par SimplGravatar herbelin2000-10-06
* Un usage en moins de l'axiome eq_rec_eqGravatar herbelin2000-10-06
* Remplacement de la tactique Program (partiel)Gravatar herbelin2000-10-05
* Commit malencontreux sur précédente versionGravatar herbelin2000-10-04
* Mise en conformité nouveau Simpl pour FixGravatar herbelin2000-10-04
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* portage RefineGravatar filliatr2000-07-20
* correctionGravatar mayero2000-07-04
* ajoutsGravatar mayero2000-07-03
* Traduction de syntaxe vers ltacGravatar delahaye2000-07-03
* Séparation des caractères spéciaux par un blancGravatar herbelin2000-07-01
* Retrait des parenthèses inutiles autour des tactiquesGravatar herbelin2000-07-01
* Require Plus ajouteGravatar filliatr2000-06-21