entetes

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

12 files changed, 84 insertions, 0 deletions

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.