let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
let relevance v = float !(v.uses) /. float !(v.nominations) in
let vcompare (_,v1) (_,v2) =
- Pervasives.compare (relevance v1) (relevance v2) in
+ Stdlib.compare (relevance v1) (relevance v2) in
let l = List.sort vcompare l in
let short_name r =
Filename.chop_extension
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)
module M =
struct
type t = int
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
;;
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
*)
let status, res = disambiguate status ctx t `XTNone in
let _,res = term_of_cic_term status res (ctx_of res)
in Ast.NCic res
- in Some ((List.map to_Ast l) @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
- Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
- Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
- Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
- ])
+ in Some (List.map to_Ast l)
+(* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases
+ @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
+ Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
+ Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
+ Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
+ ]
+*)
let auto_lowtac ~params:(univ,flags) status goal =
let gty = get_goalty status goal in