From 7b71af9c790abcff2bfe0a16a417a1023776351d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 24 Feb 2009 12:01:24 -0500
Subject: Switch to TDisjoint from CDisjoint; still need to implement
 obligation generation at EDisjoint uses

---
 src/disjoint.sig | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'src/disjoint.sig')

diff --git a/src/disjoint.sig b/src/disjoint.sig
index 0d6793c5..0d386d1a 100644
--- a/src/disjoint.sig
+++ b/src/disjoint.sig
@@ -34,12 +34,10 @@ signature DISJOINT = sig
 
     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
-- 
cgit v1.2.3