Mercurial > urweb

diff src/disjoint.sig @ 90:94ef20a31550

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fancier head normalization pushed inside of Disjoint
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 11:04:25 -0400
parents b4f2a258e52c
children 6ee1c761818f
line wrap: on
line diff
--- a/src/disjoint.sig	Tue Jul 01 16:06:58 2008 -0400
+++ b/src/disjoint.sig	Thu Jul 03 11:04:25 2008 -0400
@@ -30,9 +30,14 @@
     type env
 
     val empty : env
-    val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env
     val enter : env -> env
 
-    val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> (Elab.con * Elab.con) list
+    type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
+
+    val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env * goal list
+
+    val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> goal list
+
+    val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list
 
 end