aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Collapse)AuthorAge
...
* sumboolT, sumorT, sigTT, SigT redondantsGravatar herbelin2003-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Local 'o'Gravatar herbelin2003-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Scope en LocalGravatar herbelin2003-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement Import par Open Scope en v8Gravatar herbelin2003-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | | | | Expérience avec les notations et les scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵Gravatar herbelin2003-04-07
| | | | | | global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Espaces superflusGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Implicit Variable TypeGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des hints pour qu'Auto fasse moins de détours et lesGravatar herbelin2003-02-27
| | | | | | | | preuves soient plus naturelles. En particulier, tentative de ramener systématiquement > et >= vers < et <=. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du theoreme de CesaroGravatar desmettr2003-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3681 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour RegGravatar desmettr2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation du contenu de REALSGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans SeqPropGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans Rtrigo_defGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages nombreuxGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3586 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage f_pos -> IVT (Intermediate Value TheoremGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'un Import R_scope probablement oublieGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3582 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RListGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3580 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour renommage RcompletGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RcompleteGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage Rcomplet.v -> Rcomplete.vGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de lemmes superflusGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3576 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans PartSumGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage dans MVTGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3564 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ dans Exp_propGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3563 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage dans Binomial.vGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3562 85f007b7-540e-0410-9357-904b9bb8a0f7
* Binome.v -> Binomial.vGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3560 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ ArithPropGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage dans AltSeries.vGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3558 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage dans Alembert.vGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3557 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques améliorationsGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de INR2 / Conséquence logique de la nouvelle représentation ↵Gravatar desmettr2003-01-21
| | | | | | des constantes entières git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques optimisations...Gravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3554 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cgt définition de platGravatar desmettr2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de DiscrRGravatar desmettr2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de 'Recursive' pour les tactiques récursivesGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de 'Recursive' pour les tactiques récursivesGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clear sur hypothese non definieGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisations pour Sup et RComputeGravatar desmettr2003-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de RComputeGravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la tactique SupGravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3513 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage de TAF.v en MVT.vGravatar desmettr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 12:33:38 +0000