From 0820caf877c5b74ebcca580d7872f1f69d19274f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 23 Oct 2007 15:12:59 +0000
Subject: Enlevé les trucs commités au mauvais endroit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10252 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/biassoc.ml  | 74 ---------------------------------------------------------
 lib/biassoc.mli | 61 -----------------------------------------------
 2 files changed, 135 deletions(-)
 delete mode 100644 lib/biassoc.ml
 delete mode 100644 lib/biassoc.mli

(limited to 'lib')

diff --git a/lib/biassoc.ml b/lib/biassoc.ml
deleted file mode 100644
index 2c8fc32167..0000000000
--- a/lib/biassoc.ml
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: biassoc.ml aspiwack $ *)
-
-(* This modules implements a bidirectional association table,
-   that is a table where both values can be seen as the key for
-   the association.
-   For soundness reason, when adding an association [(a,b)] both
-   [a] and [b] must be unique.
-
-   Map is a reasonably efficient datastructure, which compares rather
-   well (in average) to the more imperative Hashtables. In that respect
-   and since persistent datastructures are used in the kernel, I write
-   this in the functional style.
-
-   This module have been originally written for being used both in the
-   retroknowledge for its internal representation (thus in the kernel)
-   and in the interactive proof system for associating dependent goals
-   to an evar. *)
-
-(* The internal representation is a straightforward pair of Maps
-   (one from a type 'a to a type 'b, and the other from the 
-   type 'b to the type 'a). Both are updated synchronously to 
-   provide fast access in both directions. *)
-
-
-
-
-type ('a,'b) biassoc = { left:('a,'b) Gmap.t ; right:('b,'a) Gmap.t }
-    
-let empty = { left=Gmap.empty ; right=Gmap.empty }
-let is_empty bm = (Gmap.is_empty bm.left)&&(Gmap.is_empty bm.right)
-  
-let find_with_left lt bm = Gmap.find lt bm.left
-let find_with_right rt bm = Gmap.find rt bm.right
-  
-let mem_with_left lt bm = Gmap.mem lt bm.left
-let mem_with_right rt bm = Gmap.mem rt bm.right
-  
-(* remove functions are not a direct lifting of the 
-   functions from either components, since you have to 
-   remove the corresponding binding in the second Map *)
-let remove_with_left lt bm = 
-  try 
-    let rt = find_with_left lt bm in
-      { left = Gmap.remove lt bm.left ;
-        right = Gmap.remove rt bm.right }
-  with Not_found ->
-    (* if there is no (lt, ?) in the left Map, then there
-       is no (?,lt) in the Right table. Thus bm is already
-       free of any reference to lt *)
-    bm
-      
-let remove_with_right rt bm = (* see remove_with_left *)
-  try 
-    let lt = find_with_right rt bm in
-      { left = Gmap.remove lt bm.left ;
-        right = Gmap.remove rt bm.right }
-  with Not_found ->
-    bm
-      
-let add lt rt bm = 
-  if not (mem_with_left lt bm) && not (mem_with_right rt bm) then
-    { left = Gmap.add lt rt bm.left ;
-      right = Gmap.add rt lt bm.right }
-  else
-    raise (Invalid_argument "Biassoc: non unique values")
-
diff --git a/lib/biassoc.mli b/lib/biassoc.mli
deleted file mode 100644
index 45426d1bc3..0000000000
--- a/lib/biassoc.mli
+++ /dev/null
@@ -1,61 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: biassoc.ml aspiwack $ *)
-
-(* This modules implements a bidirectional association table,
-   that is a table where both values can be seen as the key for
-   the association.
-   For soundness reason, when adding an association [(a,b)] both
-   [a] and [b] must be unique.
-
-   Map is a reasonably efficient datastructure, which compares rather
-   well (in average) to the more imperative Hashtables. In that respect
-   and since persistent datastructures are used in the kernel, I write
-   this in the functional style.
-
-   This module have been originally written for being used both in the
-   retroknowledge for its internal representation (thus in the kernel)
-   and in the interactive proof system for associating dependent goals
-   to an evar. *)
-
-
-
-type ('a,'b) biassoc
-(** the type of bidirectional association table between
-    ['a] and ['b] *)
-    
-val empty : ('a,'b) biassoc
-(** the empty bidirectional association table *)
-val is_empty : ('a,'b) biassoc -> bool
-(** tests the emptyness of a bidirectional association table *)
-val add : 'a -> 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [add lt rt bm] return a bidirectional association table identical 
-    to [bm] except that there is an additional association between
-    [lt] and [rt].
-    If [lt] or [rt] are already present in an association in [bm]
-    then it raises [Invalid_argument "Biassoc: non unique values"] 
-    instead *)
-val find_with_left : 'a  -> ('a,'b) biassoc -> 'b
-(** [find_with_left lt bm] returns the value associated to [lt] it 
-    there is one. It raises [Not_found] otherwise. *)
-val find_with_right : 'b -> ('a,'b) biassoc -> 'a
-(** [find_with_right] works as [find_with_left] except that
-    it implements the other direction of the association. *)
-val remove_with_left : 'a -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [remove_with_left lt bm] returns a stack identical to [bm]
-    except that any association with [lt] has been removed. *)
-val remove_with_right : 'b -> ('a,'b) biassoc -> ('a,'b) biassoc
-(** [remove_with_right] works as [remove_with_left] except that
-    the key is from the right side of the associations. *)
-val mem_with_left : 'a -> ('a,'b) biassoc -> bool
-(** [mem_with_left lt bm] returns [true] if there is a value
-    associated to [lt] in [bm]. It returns [false] otherwise. *)
-val mem_with_right : 'b -> ('a,'b) biassoc -> bool
-(** [mem_with_right] works as [mem_with_left] except that it
-    implements the other direction. *)
-- 
cgit v1.2.3