+ let continuation =
+ match ty' with
+ None -> Tacticals.id_tac
+ | Some ty' ->
+ Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+ in
+ Tacticals.thens
+ ~start:
+ (Tactics.cut ty
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:
+ [ continuation ; Tactics.apply t ]