noprint (lazy (Printf.sprintf "Refined in %fs"
(Unix.gettimeofday() -. stamp)));
let status = status#set_obj (n,h,metasenv,subst,o) in
- let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
+ let metasenv = List.filter (fun (j,_) -> j <> goal) metasenv in
let subst = (goal,(gname,ctx,pt,pty)) :: subst in
Some (status#set_obj (n,h,metasenv,subst,o))
with
NCicMetaSubst.mk_meta ~attrs:iattr
metasenv ctx ~with_type:ty ikind in
let s_entry = i,(iattr, ctx, instance, ty) in
- let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
+ let metasenv = List.filter (fun (x,_) -> i <> x) metasenv in
metasenv,s_entry::subst)
(metasenv,[]) metasenv
let (_, ctx, t, _) = List.assoc i subst in
noprint (lazy (status#ppterm ctx [] [] t));
List.iter
- (fun (uri,_,_,_,_) as obj ->
+ (fun ((uri,_,_,_,_) as obj) ->
NCicEnvironment.invalidate_item (`Obj (uri, obj)))
objs;
())
let pp_th (status: #NTacStatus.pstatus) =
List.iter
- (fun ctx, idx ->
+ (fun (ctx, idx) ->
noprint(lazy( "-----------------------------------------------"));
noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
noprint(lazy( "||====> "));
(fun elems cand ->
if (only_one && (elems <> [])) then elems
else
- match try_candidate (~smart:sm)
+ match try_candidate ~smart:sm
flags depth status cache.unit_eq context cand with
| None -> elems
| Some x -> x::elems)
debug_print ~depth
(lazy ("(re)considering goal " ^
(string_of_int g) ^" : "^ppterm status gty));
- debug_print (~depth:depth)
+ debug_print ~depth:depth
(lazy ("Case: " ^ NotationPp.pp_term status t));
let depth,cache =
if t=Ast.Ident("__whd",None) ||
let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
let flags = { flags with maxdepth = x }
in
- try auto_clusters (~top:true) flags signature cache 0 status ~use_given_only;assert false
+ try auto_clusters ~top:true flags signature cache 0 status ~use_given_only;assert false
(*
try auto_main flags signature cache 0 status;assert false
*)