From eeff794a56b9ece701932babf34a681a81d96d0b Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 20 Apr 2001 08:11:13 +0000
Subject: Ajout des entetes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1641 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/Field.v        | 10 +++++++++-
 contrib/field/Field_Compl.v  | 10 +++++++++-
 contrib/field/Field_Tactic.v | 14 +++++++++++---
 contrib/field/Field_Theory.v | 10 +++++++++-
 contrib/field/field.ml4      | 10 +++++++++-
 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
-- 
cgit v1.2.3