Mercurial > urweb
diff src/elab_util.sig @ 792:d20d6afc1206
Improvements while working on Graftid
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 12 May 2009 18:02:25 -0400 |
| parents | 7292bcb7c02d |
| children | b2413e4dd109 |
line wrap: on
line diff
--- a/src/elab_util.sig Sun May 10 10:13:41 2009 -0400 +++ b/src/elab_util.sig Tue May 12 18:02:25 2009 -0400 @@ -45,7 +45,7 @@ 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 @@ 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 @@ 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 @@ 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