comparison src/elab_ops.sig @ 623:588b9d16b00a

Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 60d97de1bbe8
children a779402841f6
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 signature ELAB_OPS = sig 28 signature ELAB_OPS = sig
29 29
30 val liftKindInKind : int -> Elab.kind -> Elab.kind
31 val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind
32
33 val liftKindInCon : int -> Elab.con -> Elab.con
34 val subKindInCon : int * Elab.kind -> Elab.con -> Elab.con
35
30 val liftConInCon : int -> Elab.con -> Elab.con 36 val liftConInCon : int -> Elab.con -> Elab.con
31 val subConInCon : int * Elab.con -> Elab.con -> Elab.con 37 val subConInCon : int * Elab.con -> Elab.con -> Elab.con
32 val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn 38 val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
33 39
34 val hnormCon : ElabEnv.env -> Elab.con -> Elab.con 40 val hnormCon : ElabEnv.env -> Elab.con -> Elab.con