comparison src/elab_util.sig @ 1639:6c00d8af6239

Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents c37d8341940a
children 4a03aa3251cb
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
62 bind : 'context * binder -> 'context} 62 bind : 'context * binder -> 'context}
63 -> 'context -> (Elab.con -> Elab.con) 63 -> 'context -> (Elab.con -> Elab.con)
64 val map : {kind : Elab.kind' -> Elab.kind', 64 val map : {kind : Elab.kind' -> Elab.kind',
65 con : Elab.con' -> Elab.con'} 65 con : Elab.con' -> Elab.con'}
66 -> Elab.con -> Elab.con 66 -> Elab.con -> Elab.con
67 val appB : {kind : 'context -> Elab.kind' -> unit,
68 con : 'context -> Elab.con' -> unit,
69 bind : 'context * binder -> 'context}
70 -> 'context -> (Elab.con -> unit)
71 val app : {kind : Elab.kind' -> unit,
72 con : Elab.con' -> unit}
73 -> Elab.con -> unit
67 val existsB : {kind : 'context * Elab.kind' -> bool, 74 val existsB : {kind : 'context * Elab.kind' -> bool,
68 con : 'context * Elab.con' -> bool, 75 con : 'context * Elab.con' -> bool,
69 bind : 'context * binder -> 'context} 76 bind : 'context * binder -> 'context}
70 -> 'context -> Elab.con -> bool 77 -> 'context -> Elab.con -> bool
71 val exists : {kind : Elab.kind' -> bool, 78 val exists : {kind : Elab.kind' -> bool,