+ let changed =
+ C.Appl [ C.Lambda (C.Name "x", tty,
+ C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
+ in
+ (* check if cutted and changed are well typed and if t1' ~ changed *)
+ let go_on =
+ try
+ let _,g = CicTypeChecker.type_of_aux' metasenv context cutted
+ CicUniv.empty_ugraph
+ in
+ let _,g = CicTypeChecker.type_of_aux' metasenv context changed g in
+ fst (CicReduction.are_convertible ~metasenv context t1' changed g)
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> false
+ in
+ if not go_on then
+ PET.apply_tactic Tacticals.id_tac status
+ else
+ (debug_print (lazy ("CUT: " ^ pp context cutted));