aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-04-10Open Scope remplace Importherbelin
2003-04-10Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterherbelin
2003-04-10Remplacement Import par Open Scope en v8herbelin
2003-04-09cast de nilherbelin
2003-04-09nil en implicite dans la v8herbelin
2003-04-09Ajout Open Scopeherbelin
2003-04-09Activation des implicites pour la v8herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-09Renommage K; equivalence JMeq et eq_dep sur Typeherbelin
2003-04-09Definedherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-07Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...herbelin
2003-04-07Cosmetiqueherbelin
2003-04-07Espaces superflusherbelin
2003-04-03Documentation, généralisation à eq sur Type, preuves d'équivalence desherbelin
2003-03-31Ajout double_plusherbelin
2003-03-31Ajout Implicit Variable Typeherbelin
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
2003-03-31Notation eqT superflueherbelin
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
2003-03-29Déplacement de minus dans Peanoherbelin
2003-03-29Implicit Variables Typeherbelin
2003-03-28Pas d'associativité gauche au niveau 3 en vieille syntaxe !herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-21*** empty log message ***barras
2003-03-14*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
2003-02-14Ajout du theoreme de Cesarodesmettr
2003-02-13Modifications dans une tactique topleveldelahaye
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
2003-01-28MAJ pour Regdesmettr
2003-01-22Documentation du contenu de REALSdesmettr
2003-01-22Modifications dans SeqPropdesmettr
2003-01-22Renommages dans Rtrigo_defdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages nombreuxdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommage f_pos -> IVT (Intermediate Value Theoremdesmettr
2003-01-22Suppression d'un Import R_scope probablement oubliedesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans RListdesmettr
2003-01-22MAJ pour renommage Rcompletdesmettr
2003-01-22Renommages dans Rcompletedesmettr
2003-01-22Renommage Rcomplet.v -> Rcomplete.vdesmettr
2003-01-22Suppression de lemmes superflusdesmettr
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans PartSumdesmettr
2003-01-22Bug precedenceherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 12:55:48 +0000