summaryrefslogtreecommitdiff
path: root/src/elab_util.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 13:35:40 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 13:35:40 -0500
commit6aaa09dfff50fdd22aeef563de63a50926bb553f (patch)
treeed45e1d909672cac6d74d612f2c9531bb71681fa /src/elab_util.sig
parentc7996285ff4b1b05a4cecdb2c1e944f7c17b18a7 (diff)
Fiddly tweaks
Diffstat (limited to 'src/elab_util.sig')
-rw-r--r--src/elab_util.sig23
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