comparison 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
comparison
equal deleted inserted replaced
1344:660a2715e2bd 1345:9e0fa4f6ac93
155 RelK of string 155 RelK of string
156 | RelC of string * Elab.kind 156 | RelC of string * Elab.kind
157 | NamedC of string * int * Elab.kind * Elab.con option 157 | NamedC of string * int * Elab.kind * Elab.con option
158 | RelE of string * Elab.con 158 | RelE of string * Elab.con
159 | NamedE of string * Elab.con 159 | NamedE of string * Elab.con
160 | Str of string * Elab.sgn 160 | Str of string * int * Elab.sgn
161 | Sgn of string * Elab.sgn 161 | Sgn of string * int * Elab.sgn
162 162
163 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, 163 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
164 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, 164 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
165 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, 165 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
166 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, 166 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
201 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, 201 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
202 str : 'context * Elab.str' * 'state -> Elab.str' * 'state, 202 str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
203 decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state, 203 decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
204 bind : 'context * binder -> 'context} 204 bind : 'context * binder -> 'context}
205 -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state 205 -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
206
207 val map : {kind : Elab.kind' -> Elab.kind',
208 con : Elab.con' -> Elab.con',
209 exp : Elab.exp' -> Elab.exp',
210 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
211 sgn : Elab.sgn' -> Elab.sgn',
212 str : Elab.str' -> Elab.str',
213 decl : Elab.decl' -> Elab.decl'}
214 -> Elab.decl -> Elab.decl
215
216 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
217 con : 'context -> Elab.con' -> Elab.con',
218 exp : 'context -> Elab.exp' -> Elab.exp',
219 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
220 sgn : 'context -> Elab.sgn' -> Elab.sgn',
221 str : 'context -> Elab.str' -> Elab.str',
222 decl : 'context -> Elab.decl' -> Elab.decl',
223 bind : 'context * binder -> 'context}
224 -> 'context -> Elab.decl -> Elab.decl
206 end 225 end
207 226
208 structure File : sig 227 structure File : sig
209 val maxName : Elab.file -> int 228 val maxName : Elab.file -> int
210 end 229 end