Skip to content

Commit 57a5ae8

Browse files
carlostomeomelkonian
authored andcommitted
Import J from Tactic
1 parent 3d94ade commit 57a5ae8

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Tactic.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ open import Tactic.Constrs public
1414
open import Tactic.EquationalReasoning public
1515
open import Tactic.Eta public
1616
open import Tactic.Intro public
17+
open import Tactic.J public
1718
open import Tactic.ReduceDec public
1819

1920
open import Tactic.Derive.DecEq public

0 commit comments

Comments
 (0)