diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
| commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
| tree | d7303613741c5796b58ced7db24ec7203327dbb2 /lib | |
| parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) | |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'lib')
43 files changed, 80 insertions, 80 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml index b33baa83..f3808f14 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: bigint.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: bigint.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (*i*) open Pp diff --git a/lib/bigint.mli b/lib/bigint.mli index 48e36875..9a890570 100644 --- a/lib/bigint.mli +++ b/lib/bigint.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: bigint.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: bigint.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/lib/bstack.ml b/lib/bstack.ml index 4afbe41e..3d549427 100644 --- a/lib/bstack.ml +++ b/lib/bstack.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: bstack.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: bstack.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Queues of a given length *) diff --git a/lib/bstack.mli b/lib/bstack.mli index b34d18d7..39a5202a 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: bstack.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: bstack.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Bounded stacks. If the depth is [None], then there is no depth limit. *) diff --git a/lib/compat.ml4 b/lib/compat.ml4 index a77c2bc6..096320ed 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/lib/dnet.ml b/lib/dnet.ml index a5b3e3df..fe20ecac 100644 --- a/lib/dnet.ml +++ b/lib/dnet.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/lib/dnet.mli b/lib/dnet.mli index 5dfc77de..eba2220b 100644 --- a/lib/dnet.mli +++ b/lib/dnet.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dyn.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: dyn.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util diff --git a/lib/dyn.mli b/lib/dyn.mli index 512baf7f..0d36dbef 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dyn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: dyn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Dynamics. Use with extreme care. Not for kids. *) diff --git a/lib/edit.ml b/lib/edit.ml index edfde186..882303a6 100644 --- a/lib/edit.ml +++ b/lib/edit.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: edit.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: edit.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/lib/edit.mli b/lib/edit.mli index 3d6f98ab..d3558716 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: edit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: edit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* The type of editors. * An editor is a finite map, ['a -> 'b], which knows how to apply diff --git a/lib/envars.ml b/lib/envars.ml index b0db1a50..f764576d 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/lib/envars.mli b/lib/envars.mli index 7370dbf5..05357b32 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/lib/explore.ml b/lib/explore.ml index c6a40e04..c40362c8 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: explore.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Format diff --git a/lib/explore.mli b/lib/explore.mli index f8180577..e01f851c 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: explore.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s Search strategies. *) diff --git a/lib/flags.ml b/lib/flags.ml index fc793780..6b68a8f2 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 13436 2010-09-19 10:18:18Z herbelin $ i*) +(*i $Id: flags.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) let with_option o f x = let old = !o in o:=true; diff --git a/lib/flags.mli b/lib/flags.mli index 75cfc96d..f4325ce2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.mli 13358 2010-07-29 23:10:17Z herbelin $ i*) +(*i $Id: flags.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Global options of the system. *) diff --git a/lib/gmap.ml b/lib/gmap.ml index 1544dacc..3f979074 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmap.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: gmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Maps using the generic comparison function of ocaml. Code borrowed from the ocaml standard library (Copyright 1996, INRIA). *) diff --git a/lib/gmap.mli b/lib/gmap.mli index 379aa63f..6da223d5 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: gmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Maps using the generic comparison function of ocaml. Same interface as the module [Map] from the ocaml standard library. *) diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 5f539971..e8dc6295 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmapl.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: gmapl.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util diff --git a/lib/gmapl.mli b/lib/gmapl.mli index 7c5d0ceb..f60aed5d 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmapl.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: gmapl.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Maps from ['a] to lists of ['b]. *) diff --git a/lib/gset.ml b/lib/gset.ml index dc88127e..28b769af 100644 --- a/lib/gset.ml +++ b/lib/gset.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gset.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: gset.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Sets using the generic comparison function of ocaml. Code borrowed from the ocaml standard library. *) diff --git a/lib/gset.mli b/lib/gset.mli index 911ff3f0..25e607f7 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gset.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: gset.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Sets using the generic comparison function of ocaml. Same interface as the module [Set] from the ocaml standard library. *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 1ebf8773..542ecde9 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hashcons.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: hashcons.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Hash consing of datastructures *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 0ce4d3b9..81c74aef 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hashcons.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: hashcons.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Generic hash-consing. *) diff --git a/lib/heap.ml b/lib/heap.ml index 47cfb46f..c61bccb9 100644 --- a/lib/heap.ml +++ b/lib/heap.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heap.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: heap.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (*s Heaps *) diff --git a/lib/heap.mli b/lib/heap.mli index e46f97ac..3183e0ec 100644 --- a/lib/heap.mli +++ b/lib/heap.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: heap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: heap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Heaps *) diff --git a/lib/option.ml b/lib/option.ml index 850d7306..f4b1604f 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: option.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: option.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. diff --git a/lib/option.mli b/lib/option.mli index c76deb3c..1dc721fe 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: option.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: option.mli 14641 2011-11-06 11:59:10Z herbelin $ *) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp_control @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp_control diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 507a54a7..a7ad553b 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp_control.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pp_control.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Parameters of pretty-printing *) diff --git a/lib/pp_control.mli b/lib/pp_control.mli index bf95bb5e..bbc771d5 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp_control.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: pp_control.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Parameters of pretty-printing. *) diff --git a/lib/profile.ml b/lib/profile.ml index 87bfe624..95163a27 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: profile.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: profile.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Gc diff --git a/lib/profile.mli b/lib/profile.mli index e61aba85..208238e7 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: profile.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: profile.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s This program is a small time and allocation profiler for Objective Caml *) diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4 index f7ddc13c..db25ce73 100644 --- a/lib/refutpat.ml4 +++ b/lib/refutpat.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/lib/rtree.ml b/lib/rtree.ml index a7428e12..991ed25c 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: rtree.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Util diff --git a/lib/rtree.mli b/lib/rtree.mli index 17cccfc8..01fff68a 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: rtree.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Type of regular tree with nodes labelled by values of type 'a *) (* The implementation uses de Bruijn indices, so binding capture diff --git a/lib/system.ml b/lib/system.ml index 7744a79b..94a57792 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 13750 2010-12-24 09:55:54Z letouzey $ *) +(* $Id: system.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -103,7 +103,7 @@ let canonical_path_name p = (* All subdirectories, recursively *) let exists_dir dir = - try let _ = opendir dir in true with Unix_error _ -> false + try let _ = closedir (opendir dir) in true with Unix_error _ -> false let skipped_dirnames = ref ["CVS"; "_darcs"] diff --git a/lib/system.mli b/lib/system.mli index 971a5c86..6998085c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: system.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: system.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tlm.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tlm.ml 14641 2011-11-06 11:59:10Z herbelin $ *) type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t diff --git a/lib/tlm.mli b/lib/tlm.mli index db3d7dd3..9042281f 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tlm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tlm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Tries. This module implements a data structure [('a,'b) t] mapping lists of values of type ['a] to sets (as lists) of values of type ['b]. *) diff --git a/lib/tries.ml b/lib/tries.ml index e7fe8a66..2540bd1e 100644 --- a/lib/tries.ml +++ b/lib/tries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |