aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* modif de la syntax: assoc a droite pour RingGravatar mayero2001-02-08
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* *** empty log message ***Gravatar mohring2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-01
* Modif de l'axiomatisation pour enlever les /\ de _neGravatar mayero2001-01-25
* Ajout d'un parseur d'entiers sous forme de patternGravatar herbelin2001-01-19
* Essai d'axiomatisation des numeralGravatar mohring2001-01-15
* Ajout de commentaire coqwebGravatar mohring2001-01-15
* corr bug -Gravatar mayero2001-01-11
* Mise a jour RbaseGravatar mohring2001-01-11
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Tactic Definition -> Meta DefinitionGravatar delahaye2001-01-09
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* *** empty log message ***Gravatar mayero2000-12-22
* Bug d'affichage à cause des << ... >>Gravatar herbelin2000-12-21
* Oublié de supprimer du code mortGravatar herbelin2000-12-20
* Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Renommages autour de NewInductionGravatar herbelin2000-12-18
* pb niveauGravatar mayero2000-12-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 03:15:32 +0000