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 /library | |
| 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 'library')
| -rw-r--r-- | library/declare.ml | 7 | ||||
| -rw-r--r-- | library/declare.mli | 7 | ||||
| -rw-r--r-- | library/global.ml | 7 | ||||
| -rw-r--r-- | library/global.mli | 7 | ||||
| -rw-r--r-- | library/goptions.ml | 7 | ||||
| -rw-r--r-- | library/goptions.mli | 7 | ||||
| -rw-r--r-- | library/impargs.ml | 7 | ||||
| -rw-r--r-- | library/impargs.mli | 7 | ||||
| -rw-r--r-- | library/indrec.ml | 7 | ||||
| -rw-r--r-- | library/indrec.mli | 7 | ||||
| -rw-r--r-- | library/lib.ml | 7 | ||||
| -rw-r--r-- | library/lib.mli | 7 | ||||
| -rw-r--r-- | library/libobject.ml | 7 | ||||
| -rw-r--r-- | library/libobject.mli | 7 | ||||
| -rw-r--r-- | library/library.ml | 7 | ||||
| -rw-r--r-- | library/library.mli | 7 | ||||
| -rwxr-xr-x | library/nametab.ml | 7 | ||||
| -rwxr-xr-x | library/nametab.mli | 7 | ||||
| -rw-r--r-- | library/states.ml | 7 | ||||
| -rw-r--r-- | library/states.mli | 7 | ||||
| -rw-r--r-- | library/summary.ml | 7 | ||||
| -rw-r--r-- | library/summary.mli | 7 |
22 files changed, 154 insertions, 0 deletions
diff --git a/library/declare.ml b/library/declare.ml index f0f2790a57..f7388133cf 100644 --- a/library/declare.ml +++ b/library/declare.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/library/declare.mli b/library/declare.mli index 6c47e3a52a..bde04bfba0 100644 --- a/library/declare.mli +++ b/library/declare.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/library/global.ml b/library/global.ml index faca388aa1..b4f45ad69c 100644 --- a/library/global.ml +++ b/library/global.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/library/global.mli b/library/global.mli index da0386be1d..c463bd1534 100644 --- a/library/global.mli +++ b/library/global.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/library/goptions.ml b/library/goptions.ml index 59d0543e22..8c0c08cefa 100644 --- a/library/goptions.ml +++ b/library/goptions.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/library/goptions.mli b/library/goptions.mli index 08f5262ebf..0129675618 100644 --- a/library/goptions.mli +++ b/library/goptions.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/library/impargs.ml b/library/impargs.ml index 8dc025e59b..4d12d9ac18 100644 --- a/library/impargs.ml +++ b/library/impargs.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/library/impargs.mli b/library/impargs.mli index bd5f6024a7..9b8d0616d9 100644 --- a/library/impargs.mli +++ b/library/impargs.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/library/indrec.ml b/library/indrec.ml index 65abfb1583..c02cb35e27 100644 --- a/library/indrec.ml +++ b/library/indrec.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/library/indrec.mli b/library/indrec.mli index 8a47c1faea..4f3cd5ee7e 100644 --- a/library/indrec.mli +++ b/library/indrec.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/library/lib.ml b/library/lib.ml index 10fd9b9655..c46a3833bf 100644 --- a/library/lib.ml +++ b/library/lib.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/library/lib.mli b/library/lib.mli index 668a65adf9..f8a126cce5 100644 --- a/library/lib.mli +++ b/library/lib.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/library/libobject.ml b/library/libobject.ml index c644cc4ebb..4f63109bfe 100644 --- a/library/libobject.ml +++ b/library/libobject.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/library/libobject.mli b/library/libobject.mli index 7b63af380a..2f68f3b279 100644 --- a/library/libobject.mli +++ b/library/libobject.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/library/library.ml b/library/library.ml index e58f716597..b30852e7d0 100644 --- a/library/library.ml +++ b/library/library.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/library/library.mli b/library/library.mli index 43fa04e8bf..e5ad55e48c 100644 --- a/library/library.mli +++ b/library/library.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/library/nametab.ml b/library/nametab.ml index 2534837916..4272bda598 100755 --- a/library/nametab.ml +++ b/library/nametab.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/library/nametab.mli b/library/nametab.mli index a62385bb66..5e867c11d5 100755 --- a/library/nametab.mli +++ b/library/nametab.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/library/states.ml b/library/states.ml index 5a4983a805..6bd8b7d647 100644 --- a/library/states.ml +++ b/library/states.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/library/states.mli b/library/states.mli index 5ff97d103e..9139c860b0 100644 --- a/library/states.mli +++ b/library/states.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/library/summary.ml b/library/summary.ml index 8fbd5efe46..c315e0cd21 100644 --- a/library/summary.ml +++ b/library/summary.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/library/summary.mli b/library/summary.mli index feca53fe37..d381543b9c 100644 --- a/library/summary.mli +++ b/library/summary.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*) |