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 62a34dbd4..0a4b51506 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 62a34dbd4..0a4b51506 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 3e8bbeeb1..8af5c310a 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 ac6511bdf..9f3865293 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 5d53cb7ef..cf6593cb3 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 3f6206c76..1427cec86 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 09025197c..4c18c5c04 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 0c821906e..d46147843 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 fe5bebc21..2f3069a1c 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 a6aec8479..a1150fb4b 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 bf2c3f9eb..3dcfbefb3 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 2c9fc7ada..b8d06acb5 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 0dbed8ffa..af840d4a6 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 7681c8aa4..8a5e146d4 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 f118bc830..434ec5464 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 188ce73d5..6d52ec4c6 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 3834fc0f5..c26cb16f9 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 af31940db..2159c36b6 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 cffc8ba7a..6ab77e008 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 61d984eb4..7ef885148 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 59adcff23..9c79507f7 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 1643c44ca..b8c0146e8 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 *)