cands, diff more_cands cands
;;
-let is_a_needed_uri s d =
- prerr_endline ("DEBUG: " ^ d ^ ": "^ s);
+let is_a_needed_uri s =
s = "cic:/matita/basics/logic/eq.ind" ||
s = "cic:/matita/basics/logic/sym_eq.con" ||
s = "cic:/matita/basics/logic/trans_eq.con" ||
if flags.local_candidates then global_cands,smart_global_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
- uri) "GLOBAL" | _ -> false)
+ uri) | _ -> false)
in filter global_cands,filter smart_global_cands
in
(* we now compute local candidates *)
if flags.local_candidates then local_cands,smart_local_cands
else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
(NUri.string_of_uri
- uri) "LOCAL" | _ -> false)
+ uri) | _ -> false)
in filter local_cands,filter smart_local_cands
in
(* we now splits candidates in facts or not facts *)
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)
+ 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)
+ ])
let auto_lowtac ~params:(univ,flags as params) status goal =
let gty = get_goalty status goal in
let ctx = ctx_of gty in
let candidates = candidates_from_ctx univ ctx status in
- auto_tac' candidates ~local_candidates:false ~use_given_only:true flags ~trace_ref:(ref [])
+ auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
let candidates = candidates_from_ctx univ [] status in