Mercurial > urweb

comparison 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
comparison
equal deleted inserted replaced
89:d3ee072fa609 90:94ef20a31550
28 signature DISJOINT = sig 28 signature DISJOINT = sig
29 29
30 type env 30 type env
31 31
32 val empty : env 32 val empty : env
33 val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env
34 val enter : env -> env 33 val enter : env -> env
35 34
36 val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> (Elab.con * Elab.con) list 35 type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
36
37 val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env * goal list
38
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
37 42
38 end 43 end