From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 lib/bigint.ml      | 4 ++--
 lib/bigint.mli     | 4 ++--
 lib/bstack.ml      | 4 ++--
 lib/bstack.mli     | 4 ++--
 lib/compat.ml4     | 2 +-
 lib/dnet.ml        | 2 +-
 lib/dnet.mli       | 2 +-
 lib/dyn.ml         | 4 ++--
 lib/dyn.mli        | 4 ++--
 lib/edit.ml        | 4 ++--
 lib/edit.mli       | 4 ++--
 lib/envars.ml      | 2 +-
 lib/envars.mli     | 2 +-
 lib/explore.ml     | 4 ++--
 lib/explore.mli    | 4 ++--
 lib/flags.ml       | 4 ++--
 lib/flags.mli      | 4 ++--
 lib/gmap.ml        | 4 ++--
 lib/gmap.mli       | 4 ++--
 lib/gmapl.ml       | 4 ++--
 lib/gmapl.mli      | 4 ++--
 lib/gset.ml        | 4 ++--
 lib/gset.mli       | 4 ++--
 lib/hashcons.ml    | 4 ++--
 lib/hashcons.mli   | 4 ++--
 lib/heap.ml        | 4 ++--
 lib/heap.mli       | 4 ++--
 lib/option.ml      | 4 ++--
 lib/option.mli     | 4 ++--
 lib/pp.ml4         | 4 ++--
 lib/pp.mli         | 4 ++--
 lib/pp_control.ml  | 4 ++--
 lib/pp_control.mli | 4 ++--
 lib/profile.ml     | 4 ++--
 lib/profile.mli    | 4 ++--
 lib/refutpat.ml4   | 2 +-
 lib/rtree.ml       | 4 ++--
 lib/rtree.mli      | 4 ++--
 lib/system.ml      | 6 +++---
 lib/system.mli     | 4 ++--
 lib/tlm.ml         | 4 ++--
 lib/tlm.mli        | 4 ++--
 lib/tries.ml       | 2 +-
 43 files changed, 80 insertions(+), 80 deletions(-)

(limited to 'lib')

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        *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 8a2a467a..2748422a 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.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: 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.
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 87c12fba..d02b5c4d 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -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
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 4b8e5a29..61b544e3 100644
--- a/lib/pp.mli
+++ b/lib/pp.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.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
diff --git a/lib/tlm.ml b/lib/tlm.ml
index aad4d363..17d337c8 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.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: 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        *)
-- 
cgit v1.2.3