diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/R_sqr.v | 10 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis.v | 10 | ||||
| -rw-r--r-- | theories/Reals/Rgeom.v | 10 | ||||
| -rw-r--r-- | theories/Reals/Rsigma.v | 12 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo.v | 10 |
5 files changed, 51 insertions, 1 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 1dfa67c8d..9fb11f2b5 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -1,3 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Require Rbase. Require DiscrR. Require Rbasic_fun. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index cdfb2fa08..38b31d7b6 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -1,3 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Require Rbase. Require Rbasic_fun. Require R_sqr. diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index eb61688b1..55bdac0bf 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -1,3 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Require Rbase. Require R_sqr. Require Rtrigo. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 5caa5a2c4..379b6485d 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -1,3 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Set Implicit Arguments. Section Sigma. @@ -69,4 +79,4 @@ Theorem sigma_eq_arg : (low:nat) (sigma low low)==(f low). Intro low; Rewrite def_sigma; [Rewrite <- (minus_n_n low); Trivial | Trivial]. Save. -End Sigma.
\ No newline at end of file +End Sigma. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 1ac4f932d..1115ec19f 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1,3 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + Require ZArith. Require Classical_Prop. Require DiscrR. |