-let by_term_we_proved t ty id ty' =
- match t with
- None -> assert false
- | Some t ->
- 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 ]
+let by_term_we_proved ~dbd t ty id ty' =
+ let just =
+ match t with
+ None -> Tactics.auto ~dbd ~params:[]
+ | Some t -> Tactics.apply t
+ in
+ 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 ; just ]