- let aux status =
- let cont,cutted =
- match ty with
- None -> Tacticals.id_tac,t
- | Some ty ->
- Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
- (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
- let proof,goals =
- ProofEngineTypes.apply_tactic
- (Tacticals.thens
- ~start:
- (Tactics.cut cutted
- ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
- ~continuations:[cont])
- status
- in
- let goals' =
- match goals with
- [fst; snd] -> [snd; fst]
- | _ -> assert false
- in
- proof,goals'
- in
- ProofEngineTypes.mk_tactic aux
+ match id with
+ None ->
+ (match ty with
+ None -> Tacticals.id_tac (*BUG: check missing here *)
+ | Some ty ->
+ Tactics.change ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (fun _ metasenv ugraph -> ty,metasenv,ugraph))
+ | Some id ->
+ let aux status =
+ let cont,cutted =
+ match ty with
+ None -> Tacticals.id_tac,t
+ | Some ty ->
+ Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph), ty in
+ let proof,goals =
+ ProofEngineTypes.apply_tactic
+ (Tacticals.thens
+ ~start:
+ (Tactics.cut cutted
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:[cont])
+ status
+ in
+ let goals' =
+ match goals with
+ [fst; snd] -> [snd; fst]
+ | _ -> assert false
+ in
+ proof,goals'
+ in
+ ProofEngineTypes.mk_tactic aux