summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
218a5af)
that must NOT be used again).
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]) status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]
]) status)
| Some lhs ->
match conclude with
]) status)
| Some lhs ->
match conclude with