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
module M =
struct
type t = int
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end
;;
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