Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
627:f4f2b09a533a 628:12b73f3c108e
32 val empty : env 32 val empty : env
33 val enter : env -> env 33 val enter : env -> env
34 34
35 type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con 35 type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
36 36
37 val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env * goal list 37 val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env
38 38
39 val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> goal list 39 val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> goal list
40
41 val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list
42 40
43 val p_env : env -> unit 41 val p_env : env -> unit
44 42
45 end 43 end