-let by_term_we_proved t ty id ty' =
-(*BUG: ty' not used *)
- match t with
- None -> assert false
- | Some t ->
- Tacticals.thens
- ~start:
- (Tactics.cut ty
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
- ~continuations:
- [ Tacticals.id_tac ; 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 ]