summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rewriting.hs-boot
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rewriting.hs-boot')
-rw-r--r--src/full/Agda/TypeChecking/Rewriting.hs-boot2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/full/Agda/TypeChecking/Rewriting.hs-boot b/src/full/Agda/TypeChecking/Rewriting.hs-boot
index 3ccbfed..26e9827 100644
--- a/src/full/Agda/TypeChecking/Rewriting.hs-boot
+++ b/src/full/Agda/TypeChecking/Rewriting.hs-boot
@@ -4,4 +4,4 @@ import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
verifyBuiltinRewrite :: Term -> Type -> TCM ()
-rewrite :: Blocked Term -> ReduceM (Either (Blocked Term) Term)
+rewrite :: Blocked_ -> Term -> RewriteRules -> Elims -> ReduceM (Reduced (Blocked Term) Term)