Bug fixed: trailing ' in names were not removed when computing the next free

name.

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index bb90cf7215ec0ed2bc85d94e6c22de69e65a4075..ea502b68592070aad0062c6002c5143059cfd0dc 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -143,11 +143,14 @@ let check_allowed_sort_elimination status localise r orig =
 let mk_fresh_name context name =
 try
  let rex = Str.regexp "[0-9']*$" in
+ let rex2 = Str.regexp "'*$" in
  let basename = Str.global_replace rex "" in
  let suffix name =
   ignore (Str.search_forward rex name 0);
   let n = Str.matched_string name in
-   if n = "" then 0 else int_of_string n in
+  let n = Str.global_replace rex2 "" n in
+   if n = "" then 0 else int_of_string n
+in
  let name' = basename name in
  let name' = if name' = "_" then "H" else name' in
  let last =