diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-12-16 13:35:40 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-12-16 13:35:40 -0500 |
commit | 6aaa09dfff50fdd22aeef563de63a50926bb553f (patch) | |
tree | ed45e1d909672cac6d74d612f2c9531bb71681fa /src/elab_util.sig | |
parent | c7996285ff4b1b05a4cecdb2c1e944f7c17b18a7 (diff) |
Fiddly tweaks
Diffstat (limited to 'src/elab_util.sig')
-rw-r--r-- | src/elab_util.sig | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/src/elab_util.sig b/src/elab_util.sig index dc0f25e8..88bdc892 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -157,8 +157,8 @@ structure Decl : sig | NamedC of string * int * Elab.kind * Elab.con option | RelE of string * Elab.con | NamedE of string * Elab.con - | Str of string * Elab.sgn - | Sgn of string * Elab.sgn + | 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, @@ -203,6 +203,25 @@ structure Decl : sig decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state, bind : 'context * binder -> 'context} -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state + + val map : {kind : Elab.kind' -> Elab.kind', + con : Elab.con' -> Elab.con', + exp : Elab.exp' -> Elab.exp', + sgn_item : Elab.sgn_item' -> Elab.sgn_item', + sgn : Elab.sgn' -> Elab.sgn', + str : Elab.str' -> Elab.str', + decl : Elab.decl' -> Elab.decl'} + -> Elab.decl -> Elab.decl + + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + exp : 'context -> Elab.exp' -> Elab.exp', + sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item', + sgn : 'context -> Elab.sgn' -> Elab.sgn', + str : 'context -> Elab.str' -> Elab.str', + decl : 'context -> Elab.decl' -> Elab.decl', + bind : 'context * binder -> 'context} + -> 'context -> Elab.decl -> Elab.decl end structure File : sig |