Ajout des entetes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1641 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 47 insertions, 7 deletions

diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index 1e5baf0167..b3261d3ea3 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -1,4 +1,12 @@
-(* Field.v *)
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id$ *)
 
 Require Export Field_Compl.
 Require Export Field_Theory.
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index d18d19f764..bcf705fb62 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -1,4 +1,12 @@
-(* Field_Compl.v *)
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id$ *)
 
 Inductive list [A:Type] : Type :=
   nil : (list A) | cons : A->(list A)->(list A).
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index d0644e8d60..f19a3d5bc2 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -1,8 +1,16 @@
-(* Field_Tactic.v *)
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id$ *)
 
 Require Ring.
-(*Require Export Field_Compl.
-Require Export Field_Theory.*)
+Require Export Field_Compl.
+Require Export Field_Theory.
 
 (**** Interpretation A --> ExprA ****)
 
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 4baa98f6bc..2cd2f09a64 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -1,4 +1,12 @@
-(* Field_Theory.v *)
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id$ *)
 
 Require Peano_dec.
 Require Ring.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 60edfe07d8..988d9dfc42 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -1,7 +1,15 @@
-(* field.ml4 *)
+(***********************************************************************)
+(*  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 camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*)
 
+(* $Id$ *)
+
 open Names
 open Proof_type
 open Tacinterp