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
---
 proofs/clenv.ml         | 7 +++++++
 proofs/clenv.mli        | 7 +++++++
 proofs/evar_refiner.ml  | 7 +++++++
 proofs/evar_refiner.mli | 7 +++++++
 proofs/logic.ml         | 7 +++++++
 proofs/logic.mli        | 7 +++++++
 proofs/pfedit.ml        | 7 +++++++
 proofs/pfedit.mli       | 7 +++++++
 proofs/proof_trees.ml   | 7 +++++++
 proofs/proof_trees.mli  | 7 +++++++
 proofs/proof_type.ml    | 7 +++++++
 proofs/proof_type.mli   | 7 +++++++
 proofs/refiner.ml       | 7 +++++++
 proofs/refiner.mli      | 7 +++++++
 proofs/tacinterp.ml     | 7 +++++++
 proofs/tacinterp.mli    | 7 +++++++
 proofs/tacmach.ml       | 7 +++++++
 proofs/tacmach.mli      | 7 +++++++
 proofs/tactic_debug.ml  | 7 +++++++
 proofs/tactic_debug.mli | 7 +++++++
 20 files changed, 140 insertions(+)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 31555eaa89..0fd86d9a3c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.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/proofs/clenv.mli b/proofs/clenv.mli
index dd8e9c31e8..59d61a5670 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 40c1f29060..ca6e2108cc 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.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/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 24ab109709..bddbc2b352 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.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/proofs/logic.ml b/proofs/logic.ml
index 0f1d2c84ca..b3800da28e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.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/proofs/logic.mli b/proofs/logic.mli
index 8591e33678..5381cffc46 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.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/proofs/pfedit.ml b/proofs/pfedit.ml
index 7ac4c07b0a..7778702495 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.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/proofs/pfedit.mli b/proofs/pfedit.mli
index 128c2b2658..3ca4ea6543 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.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/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 4a8f8dfc6c..b6867ef89f 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.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/proofs/proof_trees.mli b/proofs/proof_trees.mli
index a76eba1cbe..d579190b38 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.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/proofs/proof_type.ml b/proofs/proof_type.ml
index 3f5dbaeea7..6a22de3e64 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.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*)
 open Environ
 open Evd
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 3a9f32b639..1c9605b2e7 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.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/proofs/refiner.ml b/proofs/refiner.ml
index e9c2147536..0752b2ca95 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.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/proofs/refiner.mli b/proofs/refiner.mli
index 31dc12851e..59c5e4e4ee 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.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/proofs/tacinterp.ml b/proofs/tacinterp.ml
index cd7252c442..6b7d118ae3 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.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/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 9232d598db..fca4da9d41 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.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/proofs/tacmach.ml b/proofs/tacmach.ml
index 5ba5e0f962..81aa16c6fb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.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/proofs/tacmach.mli b/proofs/tacmach.mli
index 456398fc52..6deb243917 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.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/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index d9c5d528a7..0cdf49c70c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.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 Pp
 open Printer
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index fffe583489..aa386762b9 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.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