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 =
metasenv, subst, t, ty
with
Failure _ ->
+ let msg =
+ (lazy (localise orig_t,
+ "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+ " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
let ty = NCicReduction.whd status ~subst context ty in
+ let exn =
+ if NCicUnification.could_reduce status ~subst context ty then
+ Uncertain msg
+ else
+ RefineFailure msg
+ in
try_coercions status ~localise metasenv subst context
- t orig_t ty `Sort
- (Uncertain (lazy (localise orig_t,
- "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
- " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
+ t orig_t ty `Sort exn
and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
t (t1, t2)