Added an update function in CMap. It has the same signature as Map.add, but

expects the given key to be present, and thus is faster.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17051 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 1 deletions

diff --git a/lib/cMap.mli b/lib/cMap.mli
index 8865c1eefd..6e5f3bcfdd 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -24,9 +24,13 @@ sig
   module Set : Set.S with type elt = key
   (** Sets used by the domain function *)
 
+  val update : key -> 'a -> 'a t -> 'a t
+  (** Same as [add], but expects the key to be present, and thus faster.
+      @raise Not_found when the key is unbound in the map. *)
+
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   (** Apply the given function to the binding of the given key.
-      @raise [Not_found] when the key is unbound in the map. *)
+      @raise Not_found when the key is unbound in the map. *)
 
   val domain : 'a t -> Set.t
   (** Recover the set of keys defined in the map. *)