- Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
- (fun _ metasenv ugraph -> ty',metasenv,ugraph)
+ ty',
+ Tacticals.then_
+ ~start:
+ (Tactics.change
+ ~with_cast:true
+ ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph))
+ ~continuation:just