diff src/elab_util.sig @ 1345:9e0fa4f6ac93

Fiddly tweaks
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Dec 2010 13:35:40 -0500
parents c7b9a33c26c8
children c37d8341940a
line wrap: on
line diff
--- a/src/elab_util.sig	Thu Dec 16 10:23:37 2010 -0500
+++ b/src/elab_util.sig	Thu Dec 16 13:35:40 2010 -0500
@@ -157,8 +157,8 @@
            | 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 @@
                     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