From 187dc15532f0c6f380d7bcb07adc2180c29fedc2 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 15 Mar 2001 13:38:59 +0000
Subject: entetes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/AutoRewrite.v   | 7 +++++++
 tactics/EAuto.v         | 7 +++++++
 tactics/EqDecide.v      | 7 +++++++
 tactics/Equality.v      | 7 +++++++
 tactics/Inv.v           | 7 +++++++
 tactics/Refine.v        | 7 +++++++
 tactics/Tauto.v         | 7 +++++++
 tactics/auto.ml         | 7 +++++++
 tactics/auto.mli        | 7 +++++++
 tactics/autorewrite.ml  | 7 +++++++
 tactics/autorewrite.mli | 7 +++++++
 tactics/btermdn.ml      | 7 +++++++
 tactics/btermdn.mli     | 7 +++++++
 tactics/dhyp.ml         | 7 +++++++
 tactics/dhyp.mli        | 7 +++++++
 tactics/dn.ml           | 7 +++++++
 tactics/dn.mli          | 7 +++++++
 tactics/eauto.ml        | 7 +++++++
 tactics/elim.ml         | 7 +++++++
 tactics/elim.mli        | 7 +++++++
 tactics/eqdecide.ml     | 7 +++++++
 tactics/equality.ml     | 7 +++++++
 tactics/equality.mli    | 7 +++++++
 tactics/hiddentac.ml    | 7 +++++++
 tactics/hiddentac.mli   | 7 +++++++
 tactics/hipattern.ml    | 7 +++++++
 tactics/hipattern.mli   | 7 +++++++
 tactics/inv.ml          | 7 +++++++
 tactics/inv.mli         | 7 +++++++
 tactics/leminv.ml       | 7 +++++++
 tactics/nbtermdn.ml     | 7 +++++++
 tactics/nbtermdn.mli    | 7 +++++++
 tactics/refine.ml       | 7 +++++++
 tactics/refine.mli      | 7 +++++++
 tactics/tacentries.ml   | 7 +++++++
 tactics/tacentries.mli  | 7 +++++++
 tactics/tacticals.ml    | 7 +++++++
 tactics/tacticals.mli   | 7 +++++++
 tactics/tactics.ml      | 7 +++++++
 tactics/tactics.mli     | 7 +++++++
 tactics/tauto.ml4       | 7 +++++++
 tactics/termdn.ml       | 7 +++++++
 tactics/termdn.mli      | 7 +++++++
 tactics/wcclausenv.ml   | 7 +++++++
 tactics/wcclausenv.mli  | 7 +++++++
 45 files changed, 315 insertions(+)

(limited to 'tactics')

diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v
index 2810f4cc52..74e6d4d26f 100644
--- a/tactics/AutoRewrite.v
+++ b/tactics/AutoRewrite.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 "autorewrite".
 
 Grammar vernac orient : ast :=
diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index cb075aa79f..e1ac47ddd8 100644
--- a/tactics/EAuto.v
+++ b/tactics/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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                 The Calculus of Inductive Constructions                  *)
 (*                                                                          *)
diff --git a/tactics/EqDecide.v b/tactics/EqDecide.v
index 4fa3c2f066..05305d1b2a 100644
--- a/tactics/EqDecide.v
+++ b/tactics/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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                EqDecide.v                                *)
 (*     A tactic for deciding propositional equality on inductive types      *)
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 057e6f9003..a6e138857d 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.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       *)
+(***********************************************************************)
 
 (* $Id$: *)
 
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 62c77dc8a0..36316ec811 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.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       *)
+(***********************************************************************)
 
 (* $Id: *)
 
diff --git a/tactics/Refine.v b/tactics/Refine.v
index fe421497ff..fb73d66ee3 100644
--- a/tactics/Refine.v
+++ b/tactics/Refine.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/Tauto.v b/tactics/Tauto.v
index c6283109c1..e6b8b5e835 100644
--- a/tactics/Tauto.v
+++ b/tactics/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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 72a371267e..721ad2cf37 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 2e89462ade..bff61a8497 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.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/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f57b3f32c7..a8dc18b769 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.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       *)
+(***********************************************************************)
 open Ast
 open Coqast
 open Equality
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 2e291e5428..ce92658661 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.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/tactics/btermdn.ml b/tactics/btermdn.ml
index e238f5f79d..2b7b78d690 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ef1aaa50ae..6cccb76dd5 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.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/tactics/dhyp.ml b/tactics/dhyp.ml
index 6497287ab5..a40a748435 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 2cbf9a8270..4879bafc7b 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.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/tactics/dn.ml b/tactics/dn.ml
index b53fb26613..0e85427741 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/dn.mli b/tactics/dn.mli
index c39ab011cc..da32f853cb 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.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/tactics/eauto.ml b/tactics/eauto.ml
index 931a7a5559..2a13a9718e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 34aab19ad5..c61cdb0774 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/elim.mli b/tactics/elim.mli
index af7d17506f..e2b9a75e35 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.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/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1897a8ba6f..ae2d8a4a59 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.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/tactics/equality.ml b/tactics/equality.ml
index 726131deea..c64a869498 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index d1543e47ef..1735ebf1a0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.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/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 48b29ea5ed..2c4f80b748 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 2c45e831e0..517889c167 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.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/tactics/hipattern.ml b/tactics/hipattern.ml
index ba519cb2f2..2a2b46cba8 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 306a740439..f1a758d8ba 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.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/tactics/inv.ml b/tactics/inv.ml
index 9b81e87e6a..57d6ca7012 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index f09744c566..ed0dc1de0c 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.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/tactics/leminv.ml b/tactics/leminv.ml
index 8ca6831884..3759093f11 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 918313d0f7..abd201a3b6 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 7b7da16ef2..b056e41cf5 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.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/tactics/refine.ml b/tactics/refine.ml
index dadda64dec..9492e8eb2e 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 86d4e9c34f..f50ea12b41 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.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/tactics/tacentries.ml b/tactics/tacentries.ml
index 852b0ff832..d89f36e6bf 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index e12ed0e8ca..8c6cfebaf2 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.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/tactics/tacticals.ml b/tactics/tacticals.ml
index bef40065f6..787413d92f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e13c4758cd..aeaae6b4ef 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.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/tactics/tactics.ml b/tactics/tactics.ml
index 424b785bc1..b592fb7592 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c81e1436f9..e17806ab76 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.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/tactics/tauto.ml4 b/tactics/tauto.ml4
index 7ca436293a..a10eb70a91 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -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 camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*)
 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 4f3ea75221..4de0a8e46b 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 044cbf4ff5..fa60731f7f 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.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/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index b8bcb18ecd..1255cad54d 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index fedea84708..b7de77101c 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.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*)
 
-- 
cgit v1.2.3