aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis1.v
AgeCommit message (Collapse)Author
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
Removing in passing two Local which are no-ops in practice.
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
experiments about computing PI
2014-06-04Make standard library independent of the names generated byHugo Herbelin
induction/elim over a dependent elimination principle for Prop arguments.
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
in Prop of constructors of inductive types independent of these names. Incidentally upgraded/simplified a couple of proofs, mainly in Reals. This prepares to the next commit about using names based on H for such hypotheses in Prop.
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23Une passe sur les réels:herbelin
- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour éviter la confusion avec le Rlt_not_le de RIneq. - Quelques variantes de lemmes en plus dans RIneq. - Déplacement des énoncés de sigT dans sig (y compris la complétude) et utilisation de la notation { l:R | }. - Suppression hypothèse inutile de ln_exists1. - Ajout notation ² pour Rsqr. Au passage: - Déplacement de dec_inh_nat_subset_has_unique_least_element de ChoiceFacts vers Wf_nat. - Correction de l'espace en trop dans les notations de Specif.v liées à "&". - MAJ fichier CHANGES Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1" non prouvé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵herbelin
Rfun_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %F) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9042 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28Nommage explicite de certains "intro" pour préserver la compatibilitéherbelin
en préparation du passage à des inductifs à polymorphisme de sorte ("sigT R" va devenir de type le type de R, càd Set) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-1720 est uniquement associatif a gaucheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4672 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Pour eviter des regles redondantes en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4647 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Local 'o'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3918 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-12Open Scope en Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Remplacement Import par Open Scope en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
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
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de RealsB en Rbasedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-31MAJ pour TAFdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2950 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-29MAJ pour Rtrigo_regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2934 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2879 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-02Modification de IAF, introduction de TAF et preuves de 3 axiomesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2822 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Suppression de l'axiome d'extensionnalitedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2803 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-17Suppression de fct_eqdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2792 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11Ranalysis.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2774 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:15:01 +0000