diff options
| author | filliatr | 2001-03-15 13:38:59 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-15 13:38:59 +0000 |
| commit | 187dc15532f0c6f380d7bcb07adc2180c29fedc2 (patch) | |
| tree | d7bacf01519ca82b5745d2c493c7f7f1826106af /proofs | |
| parent | 23741168b109daece8bb588b9c5fb4506e7726ce (diff) | |
entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/clenv.mli | 7 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 7 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 7 | ||||
| -rw-r--r-- | proofs/logic.ml | 7 | ||||
| -rw-r--r-- | proofs/logic.mli | 7 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 7 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 7 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 7 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 7 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 7 | ||||
| -rw-r--r-- | proofs/refiner.ml | 7 | ||||
| -rw-r--r-- | proofs/refiner.mli | 7 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 7 | ||||
| -rw-r--r-- | proofs/tacinterp.mli | 7 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 7 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 7 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 7 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 7 |
20 files changed, 140 insertions, 0 deletions
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*) |