aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Alembert.v
AgeCommit message (Collapse)Author
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
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-03-06Add some missing Proof keywords.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-06-26Deactivate the "Standard Propositions Naming" flag, source of a lot ofHugo Herbelin
incompatibilities, at least until the check of compilation of contribs succeeds more often. Incidentally adapted some proofs in Reals which were not agnostic relatively to whether the option is on or off.
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
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
2010-02-18Removed redundant and ill-named technical lemma.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12797 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-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-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-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le ↵herbelin
traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4420 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout et MAJ commandes de scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4375 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-21Renommage dans Alembert.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3557 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-19Quelques ameliorations...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2902 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 23:07:20 +0000