commit by user andrea

[helm.git] / matita / components / ng_refiner / nCicRefiner.ml

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index d26edf6d9d3bd40783963909cc84bd9dcaaa1d13..ea502b68592070aad0062c6002c5143059cfd0dc 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t =
               ~unify:(fun m s c t1 t2 ->
                 try Some (NCicUnification.unify status m s c t1 t2)
                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
-              metasenv subst context 0 (0,NCic.Irl 0) typ
+              metasenv subst context (-1) (0,NCic.Irl 0) typ
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->
@@ -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 =