summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
9071c21)
to part was not considered because of a stupid typo.
match ty' with
None -> Tacticals.id_tac
| Some ty' ->
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:
in
Tacticals.thens
~start: