entetes

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

22 files changed, 154 insertions, 0 deletions

diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
index 62a34dbd41..0a4b515066 100644
--- a/test-suite/bench/lists-100.v
+++ b/test-suite/bench/lists-100.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       *)
+(***********************************************************************)
 Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
 Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
 Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
index 62a34dbd41..0a4b515066 100644
--- a/test-suite/bench/lists_100.v
+++ b/test-suite/bench/lists_100.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       *)
+(***********************************************************************)
 Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0.
 Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1.
 Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2.
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 3e8bbeeb17..8af5c310a2 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.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       *)
+(***********************************************************************)
 (**** Tactics Tauto and Intuition ****)
 
 (**** Tauto:
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index ac6511bdf8..9f3865293e 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.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       *)
+(***********************************************************************)
 (* Teste la verification d'unicite des noms de constr *)
 
 
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index 5d53cb7efd..cf6593cb37 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,2 +1,9 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 Fixpoint PreParadox [u:unit] : False := (PreParadox u).
 Definition Paradox := (PreParadox tt).
\ No newline at end of file
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index 3f6206c766..1427cec865 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1 +1,8 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 Check (S S).
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index 09025197c7..4c18c5c04c 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1 +1,8 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 Inductive t:Set := c: (t -> nat) -> t.
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 0c821906e0..d461478430 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,2 +1,9 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 Definition toto := Set.
 Definition toto := Set.
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index fe5bebc215..2f3069a1c1 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1 +1,8 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
 SearchPattern ? = ? outside n_existe_pas.
diff --git a/test-suite/success/Apply.v b/test-suite/success/Apply.v
index a6aec84799..a1150fb4bd 100644
--- a/test-suite/success/Apply.v
+++ b/test-suite/success/Apply.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       *)
+(***********************************************************************)
 
 (* This needs unification on type *)
 
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index bf2c3f9eb2..3dcfbefb32 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (* Pattern-matching when non inductive terms occur                          *)
 
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 2c9fc7ada8..b8d06acb54 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.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       *)
+(***********************************************************************)
 (* Compiling the theories allows to test parsing and typing but not printing *)
 (* This file tests that pretty-printing does not fail                        *)
 (* Test of exact output is not specified                                     *)
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 0dbed8ffad..af840d4a61 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.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       *)
+(***********************************************************************)
 (**** Tactics Tauto and Intuition ****)
 
 (**** Tauto:
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 7681c8aa4e..8a5e146d4e 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.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       *)
+(***********************************************************************)
 Require PolyList.
 
 Parameter in_list : (list nat*nat)->nat->Prop.
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index f118bc830c..434ec5464e 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.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       *)
+(***********************************************************************)
 
 Inductive T : Set := A: T | B :T->T.
 
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 188ce73d54..6d52ec4c64 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.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       *)
+(***********************************************************************)
 (* The "?" of cons and eq should be inferred *)
 Variable list:Set -> Set.
 Variable cons:(T:Set) T -> (list T) -> (list T).
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 3834fc0f52..c26cb16f92 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.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       *)
+(***********************************************************************)
 (* Ancien bug signale par Laurent Thery sur la condition de garde *)
 
 Require Import Bool.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index af31940db6..2159c36b60 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.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       *)
+(***********************************************************************)
 Section S.
 Inductive T [U:Type] : Set := c : U -> (T U).
 End S.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index cffc8ba7af..6ab77e0088 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.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       *)
+(***********************************************************************)
 (* Teste des definitions inductives imbriquees *)
 
 Require PolyList.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 61d984eb46..7ef885148c 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.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       *)
+(***********************************************************************)
 (* Definition mutuellement inductive et dependante *)
 
 Require Export PolyList.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 59adcff237..9c79507f7f 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.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       *)
+(***********************************************************************)
 (* Test le Hint Unfold sur des var locales *)
 
 Section toto.
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v
index 1643c44cac..b8c0146e84 100644
--- a/test-suite/tactics/TestRefine.v
+++ b/test-suite/tactics/TestRefine.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       *)
+(***********************************************************************)
 
 (* Petit bench vite fait, mal fait *)