+ 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 t id1 t1 id2 t2 =
+(*BUG: t1 and t2 not used *)
+(*PARSING BUG: t2 is parsed in the current context, but it may
+ have occurrences of id1 in it *)
+ Tactics.elim_intros t
+ ~mk_fresh_name_callback:
+ (let i = ref 0 in
+ fun _ _ _ ~typ ->
+ incr i;
+ if !i = 1 then Cic.Name id1 else Cic.Name id2)
+
+let andelim = existselim;;
+
+let rewritingstep ~dbd lhs rhs just conclude =
+ let aux ((proof,goal) as status) =
+ let (curi,metasenv,proofbo,proofty) = proof in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let eq,trans =
+ match LibraryObjects.eq_URI () with
+ None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+ | Some uri ->
+ Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])