diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-12 18:02:25 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-12 18:02:25 -0400 |
| commit | b0eb28d7ea4eb75efce79ab7493b9e21842b80b4 (patch) | |
| tree | 08ac30126986a5abd323a46c7eff436b1ac28c9f /src/elab_util.sig | |
| parent | dd6e7d3895ffed07869aa8ec6a51abaf9c602ca9 (diff) | |
Improvements while working on Graftid
Diffstat (limited to 'src/elab_util.sig')
| -rw-r--r-- | src/elab_util.sig | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/elab_util.sig b/src/elab_util.sig index 5b4bc46a..fbe208ad 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -45,7 +45,7 @@ structure Con : sig datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, @@ -79,7 +79,7 @@ structure Exp : sig datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con @@ -112,9 +112,9 @@ structure Sgn : sig datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | NamedC of string * int * Elab.kind * Elab.con option + | Str of string * int * Elab.sgn + | Sgn of string * int * Elab.sgn val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, @@ -136,13 +136,20 @@ structure Sgn : sig sgn : Elab.sgn' -> Elab.sgn'} -> Elab.sgn -> Elab.sgn + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item', + sgn : 'context -> Elab.sgn' -> Elab.sgn', + bind : 'context * binder -> 'context} + -> 'context -> Elab.sgn -> Elab.sgn + end structure Decl : sig datatype binder = RelK of string | RelC of string * Elab.kind - | NamedC of string * int * Elab.kind + | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con | Str of string * Elab.sgn |