summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
a7ac10d)
of a bottom-up conversion into a top-down conversion.
~continuation:just
)
| Some id ->
~continuation:just
)
| Some id ->
- None -> Tacticals.id_tac
- 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
in
Tacticals.thens
~start:
in
Tacticals.thens
~start:
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
- ~continuations:[ continuation ; just ]
+ ~continuations:[ Tacticals.id_tac ; continuation ]
;;
let bydone ~dbd ~universe t =
;;
let bydone ~dbd ~universe t =