From 635f559018f6a16caf5c6a75a1d38bb807e6a4c8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 16 Apr 2014 12:15:42 +0200
Subject: Fixing missing headers.

---
 theories/Reals/Machin.v     |  8 ++++++++
 theories/Reals/Ranalysis5.v | 10 +++++++++-
 theories/Reals/Ratan.v      |  8 ++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 6b91719dbb..0166ceda65 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Fourier.
 Require Import Rbase.
 Require Import Rtrigo1.
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index ba19e0a531..d876b5d8e0 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Rbase.
 Require Import Ranalysis_reg.
 Require Import Rfunctions.
@@ -1345,4 +1353,4 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
  field ; apply Rgt_not_eq ; apply Rabs_pos_lt ; assumption.
  assumption.
  field. assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 4bca627066..45a7032707 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Fourier.
 Require Import Rbase.
 Require Import PSeries_reg.
-- 
cgit v1.2.3