Mercurial > urweb
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