Mercurial > urweb
diff src/disjoint.sig @ 628:12b73f3c108e
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