Skip to content

Commit 5ff8533

Browse files
WhatisRTomelkonian
authored andcommitted
Don't reexport Reflection.Syntax from Tactic.Inline
In particular, this reexported `Type`, which you don't want if you've renamed `Set` to `Type`.
1 parent 8996a64 commit 5ff8533

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Tactic/Inline.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ open import Class.MonadTC.Instances
1818
open import Class.MonadError.Instances
1919

2020
open import Meta.Prelude
21-
open import Reflection.Syntax public
21+
open import Reflection.Syntax
2222
open import Reflection.Utils using (apply∗)
2323
open import Reflection.Utils.Debug; open Debug ("tactic.inline" , 100)
2424
-- open import Meta.Init

0 commit comments

Comments
 (0)