summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Records.hs-boot
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Records.hs-boot')
-rw-r--r--src/full/Agda/TypeChecking/Records.hs-boot4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/full/Agda/TypeChecking/Records.hs-boot b/src/full/Agda/TypeChecking/Records.hs-boot
index fb3c06a..c17e4ba 100644
--- a/src/full/Agda/TypeChecking/Records.hs-boot
+++ b/src/full/Agda/TypeChecking/Records.hs-boot
@@ -9,6 +9,6 @@ import Agda.TypeChecking.Monad
isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
isEtaRecord :: HasConstInfo m => QName -> m Bool
getRecordFieldNames :: QName -> TCM [Arg C.Name]
-etaContractRecord :: HasConstInfo m => QName -> ConHead -> Args -> m Term
+etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
isGeneratedRecordConstructor :: QName -> TCM Bool
-isRecordConstructor :: MonadTCM tcm => QName -> tcm (Maybe (QName, Defn))
+isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))