1 files changed, 6 insertions, 0 deletions
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: