~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]) status
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]) status
| Some name ->
let mk_fresh_name_callback =
fun metasenv context _ ~typ ->
~continuations:
[ Tactics.apply prhs ;
Tactics.apply (Cic.Rel 1) ;
- just]
+ Tacticals.then_
+ ~start:(Tactics.clear ~hyps:[last_hyp_name])
+ ~continuation:just]
]) status)
| Some lhs ->
match conclude with
let thesisbecomes t =
let ty = None in
- (*BUG here: missing check on t *)
match ty with
- None -> Tacticals.id_tac
+ None ->
+ Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+ (fun _ metasenv ugraph -> t,metasenv,ugraph)
| Some ty ->
+ (*BUG here: missing check on t *)
Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
(fun _ metasenv ugraph -> ty,metasenv,ugraph)
;;