Mercurial > urweb

comparison src/elab_env.sig @ 157:adc4e42e3adc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basic datatype importing works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:49:30 -0400
parents 813e5a52063d
children b4b70de488e9
comparison
equal deleted inserted replaced
156:34ccd7d2bea8 157:adc4e42e3adc
49 val pushCNamedAs : env -> string -> int -> Elab.kind -> Elab.con option -> env 49 val pushCNamedAs : env -> string -> int -> Elab.kind -> Elab.con option -> env
50 val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option 50 val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option
51 51
52 val lookupC : env -> string -> Elab.kind var 52 val lookupC : env -> string -> Elab.kind var
53 53
54 val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env
55 type datatyp
56 val lookupDatatype : env -> int -> datatyp
57 val lookupConstructor : datatyp -> int -> string * Elab.con option
58 val constructors : datatyp -> (string * int * Elab.con option) list
59
54 val pushERel : env -> string -> Elab.con -> env 60 val pushERel : env -> string -> Elab.con -> env
55 val lookupERel : env -> int -> string * Elab.con 61 val lookupERel : env -> int -> string * Elab.con
56 62
57 val pushENamed : env -> string -> Elab.con -> env * int 63 val pushENamed : env -> string -> Elab.con -> env * int
58 val pushENamedAs : env -> string -> int -> Elab.con -> env 64 val pushENamedAs : env -> string -> int -> Elab.con -> env
76 val sgiBinds : env -> Elab.sgn_item -> env 82 val sgiBinds : env -> Elab.sgn_item -> env
77 83
78 val hnormSgn : env -> Elab.sgn -> Elab.sgn 84 val hnormSgn : env -> Elab.sgn -> Elab.sgn
79 85
80 val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option 86 val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
87 val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
88 -> (string * int * Elab.con option) list option
81 val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option 89 val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
82 val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option 90 val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
83 val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option 91 val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
84 val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option 92 val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option
85 93