CicRefine.type_of_aux' metasenv context term ugraph in
(Ok (term', metasenv')),ugraph1
with
- | CicRefine.Uncertain _ ->
- debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+ | CicRefine.Uncertain s ->
+ debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
Uncertain,ugraph
| CicRefine.RefineFailure msg ->
debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"