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 cd0acbabb..345867f34 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 7e6d23e82..e67db5364 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 c67f51092..c52b0e713 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 fc646f1a4..febf7850e 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 3d6d43f8c..0bbf773b9 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 2c0587ee6..819f240b9 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 8d0b0aa27..ca41a0436 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 c86022e44..4f3b7803c 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 b79f3e820..47a6687e5 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 5f484f8e6..6350feccb 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 52af882b3..83a8cc3d6 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 a73bdba51..107e5e2d9 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 6295c4099..013b91ac3 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 23c77851b..f44fad27c 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 1dc710be0..e18e01187 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 125fbe442..f6f2a95ea 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 55405a7aa..45ef9a0f5 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 07dd8bc2b..aea23900b 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 a4e00c6b3..82ee767d3 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 576794f39..61372bfe5 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 96ef3d3de..d0730044c 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 34ebf76fc..2e8476790 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 b6d6132e0..2551726df 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 8a90abf5d..825b792d7 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 647aaea44..8d4105cf6 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 0441d2de1..ab1b608a5 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 40a83feb6..a85d7174d 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 db478d9e3..cf48f0e4b 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 a9ffd5b63..5c893eb30 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 d16353f1e..fca2db5ec 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 f04639750..1a6f61124 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 29273b169..5e10091e3 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 274d97af4..d46672a60 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*) |