module Macro_expander:sig..end
type level =
| |
Top_level |
| |
Nested |
type pat_pos =
| |
Bind |
| |
Param |
type macro_context =
| |
Ctxt_theorem |
| |
Ctxt_other |
typepat_position =level * pat_pos
module Expander:
val list_to_mac : (macro_context -> 'a -> 'b option) list ->
macro_context -> 'a -> 'b optionval list_to_bool_mac : (pat_position ->
macro_context -> 'a -> 'b option)
list ->
pat_position ->
macro_context -> 'a -> 'b option