+let candidates_from_ctx univ ctx status =
+ match univ with
+ | None -> None
+ | Some l ->
+ let to_Ast t =
+ (* FG: `XTSort here? *)
+ 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)
+ ])
+
+let auto_lowtac ~params:(univ,flags) 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: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
+ auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status
+