aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1618 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Remplacement Euclid_def Euclid_proof par Euclidmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1617 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Changement syntax pour Rinvmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1611 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Ajout de l'egalite de John Majormohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11coqwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1579 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11documentation automatique de la bibliothèque standardfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08Ajout lemmes arithmetiquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08ajout des lemmes Zimmermanmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1556 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Ajout de lemmes sur les booleensmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1508 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Introduction d'une preuve de False_recmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-26Bibliotheque Nummohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1491 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1359 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans ↵filliatr
certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1307 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-25Modif de l'axiomatisation pour enlever les /\ de _nemayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1278 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Ajout d'un parseur d'entiers sous forme de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1259 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Essai d'axiomatisation des numeralmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1253 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Ajout de commentaire coqwebmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1252 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11corr bug -mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1245 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Mise a jour Rbasemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1241 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Meta Definition -> Tactic Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1239 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Tactic Definition -> Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1237 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-22*** empty log message ***mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1197 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-21Bug d'affichage à cause des << ... >>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1182 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Oublié de supprimer du code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1171 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ↵herbelin
inductif où la constante la plus proche du Fix est prise en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1169 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Renommages autour de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15pb niveaumayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1128 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Prise en compte `?' dans les `` ``herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1077 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Reparation d'un bug de pretty-printdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1055 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-04caractere opaque des constantes repris en comptefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Remettre une section dans fast_integer pour contourner un bug de définition ↵herbelin
locale git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@990 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27La bonne modif des Unfoldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@989 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Suppression de Unfold inutile et maintenant échouantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@981 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Changement du parseur par défaut dans Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@972 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Le nouvel Induction s'appelle NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@965 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Petite simplif due au nouveau Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@939 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Ajout d'une syntaxe pour Reals.mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@937 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@903 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21ajout de theories/Wellfoundedfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Bug dans la règle de syntaxe de ex2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@867 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 00:46:04 +0000