module Tactic where

open import Tactic.Try public
open import Tactic.Rewrite public; open import Tactic.Rewrite.Tests
open import Tactic.Extra public
open import Tactic.Existentials public
open import Tactic.ByEq public
open import Tactic.Inline public

open import Tactic.AnyOf public
open import Tactic.Assumption public
open import Tactic.Case public
open import Tactic.Constrs public
open import Tactic.EquationalReasoning public
open import Tactic.Eta public
open import Tactic.Intro public
open import Tactic.ReduceDec public

open import Tactic.Derive.DecEq public
open import Tactic.Derive.Show public
open import Tactic.Derive.HsType public; open import Tactic.Derive.HsType.Tests
open import Tactic.Derive.Convertible public