entetes

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

13 files changed, 91 insertions, 0 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 9e0f23c2d0..0f9668756c 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 
 Declare ML Module "ocaml.cmo" "extraction.cmo".
 
diff --git a/contrib/extraction/close_env.ml b/contrib/extraction/close_env.ml
index 2b4c66da6c..ab303b0947 100644
--- a/contrib/extraction/close_env.ml
+++ b/contrib/extraction/close_env.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/close_env.mli b/contrib/extraction/close_env.mli
index 066bb2a6d1..bf6940d1cc 100644
--- a/contrib/extraction/close_env.mli
+++ b/contrib/extraction/close_env.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a6f46235b0..6aa5b7977c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 4c1d492c17..df5a414a1f 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/genpp.ml b/contrib/extraction/genpp.ml
index 27390de44f..55d80d8467 100644
--- a/contrib/extraction/genpp.ml
+++ b/contrib/extraction/genpp.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/genpp.mli b/contrib/extraction/genpp.mli
index 1bd795c090..376b069d0d 100644
--- a/contrib/extraction/genpp.mli
+++ b/contrib/extraction/genpp.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 525b8dc3d9..95b81fe108 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml
index 12e39d0441..6fd5d86571 100644
--- a/contrib/extraction/mlimport.ml
+++ b/contrib/extraction/mlimport.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli
index 6e302989fe..4fdb2e9eae 100644
--- a/contrib/extraction/mlimport.mli
+++ b/contrib/extraction/mlimport.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index ba7d59e724..83189ec579 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index be80e419a6..ff8dce97fe 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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*)
 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 2f06ad3972..2d40d97f52 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 
 Extraction nat.