summaryrefslogtreecommitdiff
path: root/Binaries/DafnyPrelude.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
-rw-r--r--Binaries/DafnyPrelude.bpl2
1 files changed, 2 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 342b72c1..c23e8a7e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -471,6 +471,8 @@ function DatatypeCtorId(DatatypeType): DtCtorId;
function DtRank(DatatypeType): int;
+function CoDatatypeCertificate#Equal(DatatypeType, DatatypeType): bool;
+
// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
// ---------------------------------------------------------------