diff options
Diffstat (limited to 'lib')
41 files changed, 0 insertions, 81 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml index f505bbe14e..a3462faa18 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (*i*) open Pp (*i*) diff --git a/lib/bigint.mli b/lib/bigint.mli index 06f5422278..348c6c5d9a 100644 --- a/lib/bigint.mli +++ b/lib/bigint.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp (** Arbitrary large integer numbers *) diff --git a/lib/dnet.ml b/lib/dnet.ml index f7b3692978..a0c3011453 100644 --- a/lib/dnet.ml +++ b/lib/dnet.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - (* Generic dnet implementation over non-recursive types *) module type Datatype = diff --git a/lib/dnet.mli b/lib/dnet.mli index 8b50fae239..be33ecc6aa 100644 --- a/lib/dnet.mli +++ b/lib/dnet.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id:{% $ %} *) - (** Generic discrimination net implementation over recursive types. This module implements a association data structure similar to tries but working on any types (not just lists). It is a term diff --git a/lib/dyn.ml b/lib/dyn.ml index d2bd458a7d..a2548fa697 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util (* Dynamics, programmed with DANGER !!! *) diff --git a/lib/dyn.mli b/lib/dyn.mli index befc8de7e3..235dae3aff 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Dynamics. Use with extreme care. Not for kids. *) type t diff --git a/lib/explore.ml b/lib/explore.ml index 7604950998..b227112b25 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Format (*s Definition of a search problem. *) diff --git a/lib/explore.mli b/lib/explore.mli index 34a472b72b..0e8eb32bef 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Search strategies. } *) (** {6 Sect } *) diff --git a/lib/flags.ml b/lib/flags.ml index 555739b114..cb87e2f2b6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r diff --git a/lib/flags.mli b/lib/flags.mli index 404cc2d855..8576a7e5ea 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Global options of the system. *) val boot : bool ref diff --git a/lib/gmap.ml b/lib/gmap.ml index 0c498fe7db..fc9965258a 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -5,7 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) (* Maps using the generic comparison function of ocaml. Code borrowed from the ocaml standard library (Copyright 1996, INRIA). *) diff --git a/lib/gmap.mli b/lib/gmap.mli index 7c86120c68..45b04151e9 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ 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 cec10d6444..ef8a04f289 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util type ('a,'b) t = ('a,'b list) Gmap.t diff --git a/lib/gmapl.mli b/lib/gmapl.mli index 349774073a..fdc42e3adf 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Maps from ['a] to lists of ['b]. *) type ('a,'b) t diff --git a/lib/gset.ml b/lib/gset.ml index d39cb23f25..7439e822df 100644 --- a/lib/gset.ml +++ b/lib/gset.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* 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 0b80176d51..265f8eb343 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ 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 921a4ed563..5e6f31179c 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Hash consing of datastructures *) (* The generic hash-consing functions (does not use Obj) *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index ca66730b2c..2b3b7dfb0e 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Generic hash-consing. *) module type Comp = diff --git a/lib/heap.ml b/lib/heap.ml index 7ddb4a7205..f1878f2ab9 100644 --- a/lib/heap.ml +++ b/lib/heap.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (*s Heaps *) module type Ordered = sig diff --git a/lib/heap.mli b/lib/heap.mli index a8c70d37d2..fe34b250dd 100644 --- a/lib/heap.mli +++ b/lib/heap.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Heaps *) module type Ordered = sig diff --git a/lib/option.ml b/lib/option.ml index 942fff48ae..cd145d1c30 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ 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 3711a2efd7..b37d905f56 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: option.mli 12603 2009-12-21 11:16:27Z 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 b0948b0f40..405919673b 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp_control (* This should not be used outside of this file. Use diff --git a/lib/pp.mli b/lib/pp.mli index 6ddfa6fc9c..56e66225cb 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp_control (** Modify pretty printing functions behavior for emacs ouput (special diff --git a/lib/pp_control.ml b/lib/pp_control.ml index ecc546491d..cd92cc3522 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Parameters of pretty-printing *) type pp_global_params = { diff --git a/lib/pp_control.mli b/lib/pp_control.mli index 83ee7a0f36..fe1ee6de35 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Parameters of pretty-printing. *) type pp_global_params = { diff --git a/lib/predicate.ml b/lib/predicate.ml index af66c0f28d..e419aa6e9c 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,8 +10,6 @@ (* *) (************************************************************************) -(* $Id$ *) - (* Sets over ordered types *) module type OrderedType = diff --git a/lib/predicate.mli b/lib/predicate.mli index 862479ec40..bcc89e7275 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,6 +1,4 @@ -(*i $Id$ i*) - (** Module [Pred]: sets over infinite ordered types with complement. *) (** This module implements the set data structure, given a total ordering diff --git a/lib/profile.ml b/lib/profile.ml index 78caf01484..d154478177 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Gc let word_length = Sys.word_size / 8 diff --git a/lib/profile.mli b/lib/profile.mli index 3d64b79c18..1934b04820 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 This program is a small time and allocation profiler for Objective Caml } *) (*i It requires the UNIX library *) diff --git a/lib/rtree.ml b/lib/rtree.ml index ad4d313385..b1c9345064 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util diff --git a/lib/rtree.mli b/lib/rtree.mli index 6dd66d104c..42723358d9 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Type of regular tree with nodes labelled by values of type 'a The implementation uses de Bruijn indices, so binding capture is avoided by the lift operator (see example below) *) diff --git a/lib/safe_marshal.ml b/lib/safe_marshal.ml index 88101b5d2f..e9ba81b499 100644 --- a/lib/safe_marshal.ml +++ b/lib/safe_marshal.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i) let bohcnv = Array.init 256 (fun i -> i - (if 0x30 <= i then 0x30 else 0) - diff --git a/lib/store.ml b/lib/store.ml index 8f1309531e..bc1b335fd0 100644 --- a/lib/store.ml +++ b/lib/store.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (*** This module implements an "untyped store", in this particular case we see it as an extensible record whose fields are left unspecified. ***) diff --git a/lib/store.mli b/lib/store.mli index 0caeb2abba..5df0c99a76 100644 --- a/lib/store.mli +++ b/lib/store.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (*** This module implements an "untyped store", in this particular case we see it as an extensible record whose fields are left unspecified. ***) diff --git a/lib/system.ml b/lib/system.ml index 4b657e4855..2391b99e0b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Unix diff --git a/lib/system.mli b/lib/system.mli index 8eb3758049..09142f3652 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Sect } *) (** 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 1c1483ad49..a3d4d1a03a 100644 --- a/lib/tlm.ml +++ b/lib/tlm.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t let empty = Node (Gset.empty, Gmap.empty) diff --git a/lib/tlm.mli b/lib/tlm.mli index 05ecee8713..e4c980696b 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ 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/util.ml b/lib/util.ml index ce98d32349..a70278d575 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - open Pp (* Errors *) diff --git a/lib/util.mli b/lib/util.mli index ecf6b0a165..fd8ff9275f 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 **********************************************************************) -(*i $Id$ i*) - open Pp (** This module contains numerous utility functions on strings, lists, |