+ 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
+;;
+
+let existselim ~dbd ~automation_cache just id1 t1 id2 t2 =
+ let aux (proof, goal) =
+ let (n,metasenv,_subst,bo,ty,attrs) = proof in
+ let metano,context,_ = CicUtil.lookup_meta goal metasenv in
+ let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
+ let proof' = (n,metasenv,_subst,bo,ty,attrs) in
+ ProofEngineTypes.apply_tactic (
+ Tacticals.thens
+ ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
+ ~continuations:
+ [ Tactics.elim_intros (Cic.Rel 1)
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
+ (mk_just ~dbd ~automation_cache just)
+ ]) (proof', goal)