diff src/elab_util.sig @ 711:7292bcb7c02d

Made type class system very general; demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 12:31:56 -0400
parents 588b9d16b00a
children d20d6afc1206
line wrap: on
line diff
--- a/src/elab_util.sig	Tue Apr 07 20:38:01 2009 -0400
+++ b/src/elab_util.sig	Thu Apr 09 12:31:56 2009 -0400
@@ -62,6 +62,10 @@
     val map : {kind : Elab.kind' -> Elab.kind',
                con : Elab.con' -> Elab.con'}
               -> Elab.con -> Elab.con
+    val existsB : {kind : 'context * Elab.kind' -> bool,
+                  con : 'context * Elab.con' -> bool,
+                   bind : 'context * binder -> 'context}
+                  -> 'context -> Elab.con -> bool
     val exists : {kind : Elab.kind' -> bool,
                   con : Elab.con' -> bool} -> Elab.con -> bool