4 (Tactics.intros ~howmany:1
5 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
7 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
8 (fun _ metasenv ugraph -> t,metasenv,ugraph))
14 (Tactics.intros ~howmany:1
15 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
17 (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
18 (fun _ metasenv ugraph -> t,metasenv,ugraph))
21 let by_term_we_proved t ty id =
25 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
27 [ Tacticals.id_tac ; Tactics.apply t ]
31 (Tactics.apply ~term:t)
35 let we_need_to_prove t id =
38 ProofEngineTypes.apply_tactic
40 ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
45 [fst; snd] -> [snd; fst]
50 ProofEngineTypes.mk_tactic aux