~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 _ ->
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 =