+ let reorder_pattern ((proof, goal) as status) =
+ let _,metasenv,_,_,_,_ = proof in
+ let conjecture = CicUtil.lookup_meta goal metasenv in
+ let _,context,_ = conjecture in
+ let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+ PET.apply_tactic
+ (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+ ~continuation:(PET.mk_tactic (cases_tac pattern))) status
+ in
+ PET.mk_tactic reorder_pattern