From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 6 Jun 2011 20:52:43 +0000 (+0000)
Subject: Bug fixed: trailing ' in names were not removed when computing the next free
X-Git-Tag: make_still_working~2459
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=83a494ff9e15871231c8338df95f89926f2293ba;p=helm.git

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 bb90cf721..ea502b685 100644
--- 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 =