- ~continuations:
- [injection1_tac ~first_time:false ~liftno:0 ~term:(C.Rel 1)
- ~continuation:
- (fun ~liftno:x -> continuation ~liftno:(liftno+1+x))
- (* here I need to lift all the continuations by 1;
- since I am setting back liftno to 0, I actually
- need to lift all the continuations by liftno + 1 *)
- ;T.then_
- ~start:(PET.mk_tactic
- (fun status ->
- debug_print (lazy "riempo il cut");
- let (proof, goal) = status in
- let _,metasenv,_subst,_,_, _ = proof in
- let _,context,gty =CicUtil.lookup_meta goal metasenv in
- let gty = Unshare.unshare gty in
- let new_t1' =
- match gty with
- | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
- | _ -> raise exn_injwronggoal
- in
- debug_print
- (lazy ("metto questo: " ^ pp context changed));
- debug_print
- (lazy ("al posto di questo: " ^ pp context new_t1'));
- debug_print
- (lazy ("nel goal: " ^ pp context gty));
- debug_print
- (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
- debug_print
- (lazy ("e poi rewrite con: "^pp context term));
- let rc =
- PET.apply_tactic
- (ReductionTactics.change_tac
- ~pattern:(None, [],
- Some (ProofEngineHelpers.pattern_of
- ~term:gty [new_t1']))
- (fun _ m u -> changed,m,u))
- status
- in rc
- ))
- ~continuation:
- (T.then_
- ~start:
- (EqualityTactics.rewrite_simpl_tac
- ~direction:`LeftToRight
- ~pattern:(PET.conclusion_pattern None)
- term [])
- ~continuation:EqualityTactics.reflexivity_tac)
- ])
- status)