diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /lib | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
Remove the svn-specific $Id$ annotations
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
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, |