comparison src/elab_util.sig @ 2201:1091227f535a

Unnest properly in presence of kind polymorphism
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Dec 2015 13:41:35 -0500
parents d28adceef22a
children
comparison
equal deleted inserted replaced
2200:fc1c89627178 2201:1091227f535a
39 -> (Elab.kind, 'state, 'abort) Search.mapfolder 39 -> (Elab.kind, 'state, 'abort) Search.mapfolder
40 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool 40 val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
41 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', 41 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
42 bind : 'context * string -> 'context} 42 bind : 'context * string -> 'context}
43 -> 'context -> (Elab.kind -> Elab.kind) 43 -> 'context -> (Elab.kind -> Elab.kind)
44 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
45 bind : 'context * string -> 'context}
46 -> 'context -> 'state -> Elab.kind -> 'state
44 end 47 end
45 48
46 structure Con : sig 49 structure Con : sig
47 datatype binder = 50 datatype binder =
48 RelK of string 51 RelK of string