- | _ 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)