diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bij.ml | 7 | ||||
| -rw-r--r-- | lib/bij.mli | 7 | ||||
| -rw-r--r-- | lib/bstack.ml | 7 | ||||
| -rw-r--r-- | lib/bstack.mli | 7 | ||||
| -rw-r--r-- | lib/dyn.ml | 7 | ||||
| -rw-r--r-- | lib/dyn.mli | 7 | ||||
| -rw-r--r-- | lib/edit.ml | 7 | ||||
| -rw-r--r-- | lib/edit.mli | 7 | ||||
| -rw-r--r-- | lib/explore.ml | 7 | ||||
| -rw-r--r-- | lib/explore.mli | 7 | ||||
| -rw-r--r-- | lib/gmap.ml | 7 | ||||
| -rw-r--r-- | lib/gmap.mli | 7 | ||||
| -rw-r--r-- | lib/gmapl.ml | 7 | ||||
| -rw-r--r-- | lib/gmapl.mli | 7 | ||||
| -rw-r--r-- | lib/gset.ml | 7 | ||||
| -rw-r--r-- | lib/gset.mli | 7 | ||||
| -rw-r--r-- | lib/hashcons.ml | 7 | ||||
| -rw-r--r-- | lib/hashcons.mli | 7 | ||||
| -rw-r--r-- | lib/options.ml | 7 | ||||
| -rw-r--r-- | lib/options.mli | 7 | ||||
| -rw-r--r-- | lib/pp.ml | 7 | ||||
| -rw-r--r-- | lib/pp.mli | 7 | ||||
| -rw-r--r-- | lib/pp_control.ml | 7 | ||||
| -rw-r--r-- | lib/pp_control.mli | 7 | ||||
| -rw-r--r-- | lib/profile.ml | 7 | ||||
| -rw-r--r-- | lib/profile.mli | 7 | ||||
| -rw-r--r-- | lib/stamps.ml | 7 | ||||
| -rw-r--r-- | lib/stamps.mli | 7 | ||||
| -rw-r--r-- | lib/system.ml | 7 | ||||
| -rw-r--r-- | lib/system.mli | 7 | ||||
| -rw-r--r-- | lib/tlm.ml | 7 | ||||
| -rw-r--r-- | lib/tlm.mli | 7 | ||||
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 7 |
34 files changed, 238 insertions, 0 deletions
diff --git a/lib/bij.ml b/lib/bij.ml index cd0acbabbb..345867f34b 100644 --- a/lib/bij.ml +++ b/lib/bij.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/lib/bij.mli b/lib/bij.mli index 7e6d23e828..e67db5364c 100644 --- a/lib/bij.mli +++ b/lib/bij.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/lib/bstack.ml b/lib/bstack.ml index c67f51092c..c52b0e713a 100644 --- a/lib/bstack.ml +++ b/lib/bstack.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/lib/bstack.mli b/lib/bstack.mli index fc646f1a4f..febf7850ed 100644 --- a/lib/bstack.mli +++ b/lib/bstack.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/lib/dyn.ml b/lib/dyn.ml index 3d6d43f8c4..0bbf773b9b 100644 --- a/lib/dyn.ml +++ b/lib/dyn.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/lib/dyn.mli b/lib/dyn.mli index 2c0587ee67..819f240b9e 100644 --- a/lib/dyn.mli +++ b/lib/dyn.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/lib/edit.ml b/lib/edit.ml index 8d0b0aa276..ca41a04365 100644 --- a/lib/edit.ml +++ b/lib/edit.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/lib/edit.mli b/lib/edit.mli index c86022e443..4f3b7803c1 100644 --- a/lib/edit.mli +++ b/lib/edit.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/lib/explore.ml b/lib/explore.ml index b79f3e8207..47a6687e5d 100644 --- a/lib/explore.ml +++ b/lib/explore.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/lib/explore.mli b/lib/explore.mli index 5f484f8e6a..6350feccba 100644 --- a/lib/explore.mli +++ b/lib/explore.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/lib/gmap.ml b/lib/gmap.ml index 52af882b35..83a8cc3d69 100644 --- a/lib/gmap.ml +++ b/lib/gmap.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$ *) (* Maps using the generic comparison function of ocaml. Code borrowed from diff --git a/lib/gmap.mli b/lib/gmap.mli index a73bdba519..107e5e2d99 100644 --- a/lib/gmap.mli +++ b/lib/gmap.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/lib/gmapl.ml b/lib/gmapl.ml index 6295c4099c..013b91ac34 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.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/lib/gmapl.mli b/lib/gmapl.mli index 23c77851bc..f44fad27c0 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.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/lib/gset.ml b/lib/gset.ml index 1dc710be0b..e18e01187f 100644 --- a/lib/gset.ml +++ b/lib/gset.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/lib/gset.mli b/lib/gset.mli index 125fbe4422..f6f2a95eaa 100644 --- a/lib/gset.mli +++ b/lib/gset.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/lib/hashcons.ml b/lib/hashcons.ml index 55405a7aaf..45ef9a0f53 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.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/lib/hashcons.mli b/lib/hashcons.mli index 07dd8bc2b0..aea23900b1 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.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/lib/options.ml b/lib/options.ml index a4e00c6b37..82ee767d34 100644 --- a/lib/options.ml +++ b/lib/options.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/lib/options.mli b/lib/options.mli index 576794f39c..61372bfe5e 100644 --- a/lib/options.mli +++ b/lib/options.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*) @@ -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/lib/pp.mli b/lib/pp.mli index 96ef3d3ded..d0730044c1 100644 --- a/lib/pp.mli +++ b/lib/pp.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/lib/pp_control.ml b/lib/pp_control.ml index 34ebf76fc5..2e84767901 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.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/lib/pp_control.mli b/lib/pp_control.mli index b6d6132e01..2551726df3 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.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/lib/profile.ml b/lib/profile.ml index 8a90abf5de..825b792d7d 100644 --- a/lib/profile.ml +++ b/lib/profile.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/lib/profile.mli b/lib/profile.mli index 647aaea44c..8d4105cf6a 100644 --- a/lib/profile.mli +++ b/lib/profile.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/stamps.ml b/lib/stamps.ml index 0441d2de16..ab1b608a54 100644 --- a/lib/stamps.ml +++ b/lib/stamps.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/lib/stamps.mli b/lib/stamps.mli index 40a83feb69..a85d7174d3 100644 --- a/lib/stamps.mli +++ b/lib/stamps.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/lib/system.ml b/lib/system.ml index db478d9e35..cf48f0e4b4 100644 --- a/lib/system.ml +++ b/lib/system.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/lib/system.mli b/lib/system.mli index a9ffd5b63e..5c893eb30e 100644 --- a/lib/system.mli +++ b/lib/system.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/lib/tlm.ml b/lib/tlm.ml index d16353f1ec..fca2db5ec7 100644 --- a/lib/tlm.ml +++ b/lib/tlm.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/lib/tlm.mli b/lib/tlm.mli index f046397504..1a6f611241 100644 --- a/lib/tlm.mli +++ b/lib/tlm.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/lib/util.ml b/lib/util.ml index 29273b1690..5e10091e3f 100644 --- a/lib/util.ml +++ b/lib/util.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/lib/util.mli b/lib/util.mli index 274d97af41..d46672a603 100644 --- a/lib/util.mli +++ b/lib/util.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*) |