+ if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
+;;
+
+let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
+ let gty = get_goalty status goal in
+ let eq status ctx t1 t2 =
+ let status,t1 = disambiguate status t1 None ctx in
+ let status,t1 = apply_subst status ctx t1 in
+ let status,t1 = term_of_cic_term status t1 ctx in
+ let t2 = mk_cic_term ctx t2 in
+ let status,t2 = apply_subst status ctx t2 in
+ let status,t2 = term_of_cic_term status t2 ctx in
+ prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2);
+ assert (t1=t2);
+ status
+ in
+ let status,gty' = term_of_cic_term status gty (ctx_of gty) in
+ let status = eq status (ctx_of gty) concl gty' in
+ let status,_ =
+ List.fold_right2
+ (fun (id1,e1) ((id2,e2) as item) (status,ctx) ->
+ assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false));
+ match e1,e2 with
+ `Decl t1, NCic.Decl t2 ->
+ let status = eq status ctx t1 t2 in
+ status,item::ctx
+ | `Def (b1,t1), NCic.Def (b2,t2) ->
+ let status = eq status ctx t1 t2 in
+ let status = eq status ctx b1 b2 in
+ status,item::ctx
+ | _ -> assert false
+ ) hyps (ctx_of gty) (status,[])
+ in
+ exec id_tac status goal)
+;;
+
+let assert_tac seqs status =
+ match status.gstatus with
+ | [] -> assert false
+ | (g,_,_,_) :: s ->
+ assert (List.length g = List.length seqs);
+ (match seqs with
+ [] -> id_tac
+ | [seq] -> assert0_tac seq
+ | _ ->
+ block_tac
+ (branch_tac::
+ HExtlib.list_concat ~sep:[shift_tac]
+ (List.map (fun seq -> [assert0_tac seq]) seqs)@
+ [merge_tac])
+ ) status
+;;
+
+let auto ~params status goal =
+ let gty = get_goalty status goal in
+ let n,h,metasenv,subst,o = status.pstatus in
+ let status,t = term_of_cic_term status gty (ctx_of gty) in
+ Paramod.nparamod metasenv subst (ctx_of gty) t;
+ status
+;;
+
+let auto_tac ~params status =
+ distribute_tac (auto ~params) status