in
PET.mk_tactic subst_tac
-and destruct ?(simplified = false) ~first_time term =
+and destruct ~first_time term =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
in
| _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
mk_subst_chain `RightToLeft i2 t1 t2
(* else part *)
- | _ when first_time && simplified -> raise exn_nothingtodo
- | _ when simplified (* && not first time *) -> T.id_tac
- | _ (* when not simplified *) ->
- T.then_ ~start:(simpl_in_term context term)
- ~continuation:(destruct ~simplified:true ~first_time term)
+ | _ when first_time -> raise exn_nothingtodo
+ | _ (* when not first time *) -> T.id_tac
end
- | _ when first_time && simplified -> raise exn_nothingtodo
- | _ when simplified (* && not first time *) -> T.id_tac
- | _ (* when not simplified *) ->
- T.then_ ~start:(simpl_in_term context term)
- ~continuation:(destruct ~simplified:true ~first_time term)
+ | _ when first_time -> raise exn_nothingtodo
+ | _ (* when not first time *) -> T.id_tac
in
PET.apply_tactic tac status
in