summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml4
-rw-r--r--lib/bigint.mli4
-rw-r--r--lib/bstack.ml4
-rw-r--r--lib/bstack.mli4
-rw-r--r--lib/compat.ml42
-rw-r--r--lib/dnet.ml2
-rw-r--r--lib/dnet.mli2
-rw-r--r--lib/dyn.ml4
-rw-r--r--lib/dyn.mli4
-rw-r--r--lib/edit.ml4
-rw-r--r--lib/edit.mli4
-rw-r--r--lib/envars.ml2
-rw-r--r--lib/envars.mli2
-rw-r--r--lib/explore.ml4
-rw-r--r--lib/explore.mli4
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli4
-rw-r--r--lib/gmap.ml4
-rw-r--r--lib/gmap.mli4
-rw-r--r--lib/gmapl.ml4
-rw-r--r--lib/gmapl.mli4
-rw-r--r--lib/gset.ml4
-rw-r--r--lib/gset.mli4
-rw-r--r--lib/hashcons.ml4
-rw-r--r--lib/hashcons.mli4
-rw-r--r--lib/heap.ml4
-rw-r--r--lib/heap.mli4
-rw-r--r--lib/option.ml4
-rw-r--r--lib/option.mli4
-rw-r--r--lib/pp.ml44
-rw-r--r--lib/pp.mli4
-rw-r--r--lib/pp_control.ml4
-rw-r--r--lib/pp_control.mli4
-rw-r--r--lib/profile.ml4
-rw-r--r--lib/profile.mli4
-rw-r--r--lib/refutpat.ml42
-rw-r--r--lib/rtree.ml4
-rw-r--r--lib/rtree.mli4
-rw-r--r--lib/system.ml6
-rw-r--r--lib/system.mli4
-rw-r--r--lib/tlm.ml4
-rw-r--r--lib/tlm.mli4
-rw-r--r--lib/tries.ml2
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 *)
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 *)