Rename update to set, fixes #6196

4 files changed, 29 insertions, 15 deletions

diff --git a/lib/cMap.ml b/lib/cMap.ml
index 0ecb40209..b4c4aedd0 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -26,7 +26,7 @@ sig
   include CSig.MapS
   module Set : CSig.SetS with type elt = key
   val get : key -> 'a t -> 'a
-  val update : key -> 'a -> 'a t -> 'a t
+  val set : key -> 'a -> 'a t -> 'a t
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   val domain : 'a t -> Set.t
   val bind : (key -> 'a) -> Set.t -> 'a t
@@ -50,7 +50,7 @@ end
 module MapExt (M : Map.OrderedType) :
 sig
   type 'a map = 'a Map.Make(M).t
-  val update : M.t -> 'a -> 'a map -> 'a map
+  val set : M.t -> 'a -> 'a map -> 'a map
   val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map
   val domain : 'a map -> Set.Make(M).t
   val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map
@@ -93,19 +93,19 @@ struct
   let set_prj : set -> _set = Obj.magic
   let set_inj : _set -> set = Obj.magic
 
-  let rec update k v (s : 'a map) : 'a map = match map_prj s with
+  let rec set k v (s : 'a map) : 'a map = match map_prj s with
   | MEmpty -> raise Not_found
   | MNode (l, k', v', r, h) ->
     let c = M.compare k k' in
     if c < 0 then
-      let l' = update k v l in
+      let l' = set k v l in
       if l == l' then s
       else map_inj (MNode (l', k', v', r, h))
     else if c = 0 then
       if v' == v then s
       else map_inj (MNode (l, k', v, r, h))
     else
-      let r' = update k v r in
+      let r' = set k v r in
       if r == r' then s
       else map_inj (MNode (l, k', v', r', h))
 
diff --git a/lib/cMap.mli b/lib/cMap.mli
index f65036139..5e65bd200 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -34,7 +34,7 @@ sig
   val get : key -> 'a t -> 'a
   (** Same as {!find} but fails an assertion instead of raising [Not_found] *)
 
-  val update : key -> 'a -> 'a t -> 'a t
+  val set : 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. *)
 
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 6910cbbf0..32e9d2af0 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -56,6 +56,12 @@ sig
     val is_empty: 'a t -> bool
     val mem: key -> 'a t -> bool
     val add: key -> 'a -> 'a t -> 'a t
+    (* when Coq requires OCaml 4.06 or later, can add:
+
+         val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
+
+       allowing Coq to use OCaml's "update"
+    *)
     val singleton: key -> 'a -> 'a t
     val remove: key -> 'a t -> 'a t
     val merge:
diff --git a/lib/hMap.ml b/lib/hMap.ml
index c69efdb71..37079af78 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -47,7 +47,7 @@ struct
     try
       let m = Int.Map.find h s in
       let m = Set.add x m in
-      Int.Map.update h m s
+      Int.Map.set h m s
     with Not_found ->
       let m = Set.singleton x in
       Int.Map.add h m s
@@ -65,7 +65,7 @@ struct
       if Set.is_empty m then
         Int.Map.remove h s
       else
-        Int.Map.update h m s
+        Int.Map.set h m s
     with Not_found -> s
 
   let height s = Int.Map.height s
@@ -135,7 +135,7 @@ struct
         let s' = Int.Map.find h accu in
         let si = Set.filter (fun e -> not (Set.mem e s)) s' in
         if Set.is_empty si then Int.Map.remove h accu
-        else Int.Map.update h si accu
+        else Int.Map.set h si accu
      with Not_found -> accu
     in
     Int.Map.fold fold s2 s1
@@ -242,11 +242,19 @@ struct
     try
       let m = Int.Map.find h s in
       let m = Map.add k x m in
-      Int.Map.update h m s
+      Int.Map.set h m s
     with Not_found ->
       let m = Map.singleton k x in
       Int.Map.add h m s
 
+  (* when Coq requires OCaml 4.06 or later, the module type
+     CSig.MapS may include the signature of OCaml's "update",
+     requiring an implementation here, which could be just:
+
+       let update k f s = assert false (* not implemented *)
+
+  *)
+
   let singleton k x =
     let h = M.hash k in
     Int.Map.singleton h (Map.singleton k x)
@@ -259,7 +267,7 @@ struct
       if Map.is_empty m then
         Int.Map.remove h s
       else
-        Int.Map.update h m s
+        Int.Map.set h m s
     with Not_found -> s
 
   let merge f s1 s2 =
@@ -359,7 +367,7 @@ struct
     let h = M.hash k in
     let m = Int.Map.find h s in
     let m = Map.modify k f m in
-    Int.Map.update h m s
+    Int.Map.set h m s
 
   let bind f s =
     let fb m = Map.bind f m in
@@ -367,11 +375,11 @@ struct
 
   let domain s = Int.Map.map Map.domain s
 
-  let update k x s =
+  let set k x s =
     let h = M.hash k in
     let m = Int.Map.find h s in
-    let m = Map.update k x m in
-    Int.Map.update h m s
+    let m = Map.set k x m in
+    Int.Map.set h m s
 
   let smartmap f s =
     let fs m = Map.smartmap f m in