Mercurial > urweb
diff src/elab_env.sig @ 191:aa54250f58ac
Parametrized datatypes through explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 08 Aug 2008 10:28:32 -0400 |
| parents | 8e9f97508f0d |
| children | e86411f647c6 |
line wrap: on
line diff
--- a/src/elab_env.sig Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab_env.sig Fri Aug 08 10:28:32 2008 -0400 @@ -51,13 +51,14 @@ val lookupC : env -> string -> Elab.kind var - val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env + val pushDatatype : env -> int -> string list -> (string * int * Elab.con option) list -> env type datatyp val lookupDatatype : env -> int -> datatyp val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option + val datatypeArgs : datatyp -> string list val constructors : datatyp -> (string * int * Elab.con option) list - val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option + val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option val pushERel : env -> string -> Elab.con -> env val lookupERel : env -> int -> string * Elab.con @@ -87,9 +88,9 @@ val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } - -> (string * int * Elab.con option) list option + -> (string list * (string * int * Elab.con option) list) option val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } - -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option + -> (Elab.datatype_kind * int * string list * Elab.con option * Elab.con) option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option