summaryrefslogtreecommitdiff
path: root/src/core_util.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-03-16 10:09:01 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-03-16 10:09:01 -0400
commite5e7bbaaae9cde0981c77e488a29e730876964ba (patch)
tree32012eb864854a36e74947956e1133ce84cd64a7 /src/core_util.sig
parenta00e028f21afd87ef9dd3ed143f52fe648275d45 (diff)
Undo an Especialize change that turned out to be unecessary
Diffstat (limited to 'src/core_util.sig')
-rw-r--r--src/core_util.sig5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/core_util.sig b/src/core_util.sig
index 807b477b..835577a3 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -73,6 +73,11 @@ structure Con : sig
val exists : {kind : Core.kind' -> bool,
con : Core.con' -> bool} -> Core.con -> bool
+
+ val existsB : {kind : 'context * Core.kind' -> bool,
+ con : 'context * Core.con' -> bool,
+ bind : 'context * binder -> 'context}
+ -> 'context -> Core.con -> bool
val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
con : Core.con' * 'state -> Core.con' * 'state}