COMMENT: was added to "Nameops.increment_suffix".

2 files changed, 39 insertions, 2 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index f3c257001..6020db33d 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -67,8 +67,20 @@ let root_of_id id =
   let suffixstart = cut_ident true id in
   Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
 
-(* Rem: semantics is a bit different, if an ident starts with toto00 then
-  after successive renamings it comes to toto09, then it goes on with toto10 *)
+(* Return the same identifier as the original one but whose {i subscript} is incremented.
+   If the original identifier does not have a suffix, [0] is appended to it.
+
+   Example mappings:
+
+   [bar]   ↦ [bar0]
+   [bar0]  ↦ [bar1]
+   [bar00] ↦ [bar01]
+   [bar1]  ↦ [bar2]
+   [bar01] ↦ [bar01]
+   [bar9]  ↦ [bar10]
+   [bar09] ↦ [bar10]
+   [bar99] ↦ [bar100]
+*)
 let increment_subscript id =
   let id = Id.to_string id in
   let len = String.length id in
diff --git a/library/nameops.mli b/library/nameops.mli
index a1ea0231f..3a67b61a1 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -21,8 +21,33 @@ val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
 val add_suffix : Id.t -> string -> Id.t
 val add_prefix : string -> Id.t -> Id.t
 
+(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)
+
 val has_subscript       : Id.t -> bool
+
 val increment_subscript : Id.t -> Id.t
+(** Return the same identifier as the original one but whose {i subscript} is incremented.
+    If the original identifier does not have a suffix, [0] is appended to it.
+
+    Example mappings:
+
+    [bar]   ↦ [bar0]
+
+    [bar0]  ↦ [bar1]
+
+    [bar00] ↦ [bar01]
+
+    [bar1]  ↦ [bar2]
+
+    [bar01] ↦ [bar01]
+
+    [bar9]  ↦ [bar10]
+
+    [bar09] ↦ [bar10]
+
+    [bar99] ↦ [bar100]
+*)
+
 val forget_subscript    : Id.t -> Id.t
 
 val out_name : Name.t -> Id.t