Mercurial > urweb

diff src/disjoint.sig @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 6ee1c761818f
children a779402841f6
line wrap: on
line diff
--- a/src/disjoint.sig	Sun Feb 22 17:39:55 2009 -0500
+++ b/src/disjoint.sig	Tue Feb 24 12:01:24 2009 -0500
@@ -34,12 +34,10 @@
 
     type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
 
-    val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env * goal list
+    val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env
 
     val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> goal list
 
-    val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list
-
     val p_env : env -> unit
 
 end