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)
+ Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> ty',metasenv,ugraph)
in
Tacticals.thens
~start: