diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /theories/Reals | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
Remove the svn-specific $Id$ annotations
- 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
Diffstat (limited to 'theories/Reals')
55 files changed, 0 insertions, 109 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index ef75323e0..1b9be0795 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index cccc8ceec..9c29e26a3 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index f22ff5cb2..48324e8e8 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rbasic_fun. Require Import Even. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 0d34d22c5..d0df984a1 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import PartSum. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 6ea0767d0..68a842c9f 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 6c08356a7..c5e2c0ed3 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 7a893c53c..d27e0ae4c 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index e037c77b5..0d41b5900 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import RIneq. Require Import Omega. Open Local Scope R_scope. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 1c74f55a0..287057f0f 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v index 774a0bd5c..eba81ff9b 100644 --- a/theories/Reals/Integration.v +++ b/theories/Reals/Integration.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export NewtonInt. Require Export RiemannInt_SF. Require Export RiemannInt.
\ No newline at end of file diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v index b33274af9..ca7cb8fea 100644 --- a/theories/Reals/LegacyRfield.v +++ b/theories/Reals/LegacyRfield.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Raxioms. Require Export LegacyField. Import LegacyRing_theory. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 4037e3dec..72bd62a69 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 74bcf7dcd..0d75a9dee 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 97793386d..80a5b87a8 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 6a33b8092..e9a224b97 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 2b6af10ec..7c4555605 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** * Basic lemmas for the classical real numbers *) (*********************************************************) diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 545bd68b2..8cf56cd7b 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Open Local Scope R_scope. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 57b2c7675..e530070b1 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (**********************************************************) (** Complements for the reals.Integer and fractional part *) (* *) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 6460a9271..1cccb8848 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rbasic_fun. Open Local Scope R_scope. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2c43ee9b9..13232566f 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rsqrt_def. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 500dd5295..53267174b 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rtrigo. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 1516b3384..a0b10c891 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Export Rlimit. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 1d44b3e73..04c00cb30 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 3b685cd8a..28da1c7c4 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 1ed3fb713..abf0b883f 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 9715414f5..1ed75cdb6 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Axiomatisation of the classical reals *) (*********************************************************) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index ab1c07474..8843c5e6e 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Rdefinitions. Require Export Raxioms. Require Export RIneq. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 7588020c5..2e1bd0797 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Complements for the real numbers *) (* *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 27d5c49ef..de3250529 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 023cfc93c..ab6ed8b10 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definitions for the axiomatization *) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 6413943a9..19ebcd3cb 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definition of the derivative,continuity *) (* *) diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index d18213db4..de57a5af2 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** The library REALS is divided in 6 parts : - Rbase: basic lemmas on R equalities and inequalities diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 7371c8acf..668891369 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 8890cbb50..dceb98d45 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 9fd6e0088..abf817d7a 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rfunctions. Require Import SeqSeries. Require Import Ranalysis. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index f9b1b890f..f783d1d82 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 3aaa7300a..e0f47364f 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definition of the limit *) (* *) diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index c7d1893be..f922e25f6 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import Rdefinitions. Fixpoint pow (r:R) (n:nat) : R := diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a4feed8f3..957466cbe 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) (*i Due to L.Thery i*) (************************************************************) diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index bb3df6bb8..4e3f4d089 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Compare. Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 1ed6b03c5..9e5122062 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Compare. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 917592702..155577746 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 33c20355c..a8f12a6b3 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Sumbool. Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 5b55896b1..a086cfd46 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 4981d6fdf..582b6be75 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index fe2da8391..1cf0944c0 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index a7fddb473..33ea1adba 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 9588e4438..265dae9d4 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index cb53b5346..62d8d9f5f 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 5b731488b..f38e59e82 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 82647c837..642e7fc9e 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index dbfc85bb9..dcfadd566 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Max. diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index 5882f953c..90048e50d 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbasic_fun. Ltac split_case_Rabs := diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 51e54860d..322808f9b 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 4f336648b..3961b8b0c 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. |