aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Ranalysis3.v
AgeCommit message (Collapse)Author
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-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
There are two main issues. First, (-cst)%R is no longer syntactically equal to (-(cst))%R (though they are still convertible). This breaks some rewriting rules. Second, the ring/field_simplify tactics did not know how to refold real constants. This defect is no longer hidden by the pretty-printer, which makes these tactics almost unusable on goals containing large constants. This commit also modifies the ring/field tactics so that real constant reification is now constant time rather than linear. Note that there is now a bit of code duplication between z_syntax and r_syntax. This should be fixed once plugin interdependencies are supported. Ideally the r_syntax plugin should just disappear by declaring IZR as a coercion. Unfortunately the coercion mechanism is not powerful enough yet, be it for parsing (need the ability for a scope to delegate constant parsing to another scope) or printing (too many visible coercions left).
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
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
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-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 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-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-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-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
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 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-22Suppression de lemmes superflusdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3576 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
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 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-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 18:54:57 +0000