Commit 801249ee authored by Andrei Paskevich's avatar Andrei Paskevich

fix parsing of metas to allow passing type symbol arguments

parent 29d5c925
......@@ -160,6 +160,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
Ty.ty_app ts (List.map ty_of_pty tyl)
in
let convert = function
| PMAty (PTyapp (q,[]))
-> MAts (find_ts th q)
| PMAty ty -> MAty (ty_of_pty ty)
| PMAfs q -> MAls (find_fs th q)
| PMAps q -> MAls (find_ps th q)
......
......@@ -1043,6 +1043,8 @@ let add_decl loc th = function
add_prop (prop_kind k) loc s f th
| Meta (id, al) ->
let convert = function
| PMAty (PPTtyapp (q,[]))
-> MAts (find_tysymbol q th)
| PMAty ty -> MAty (ty_of_pty th ty)
| PMAfs q -> MAls (find_fsymbol q th)
| PMAps q -> MAls (find_psymbol q th)
......
......@@ -127,6 +127,8 @@ let load_driver lib file extra_files =
Ty.ty_app ts (List.map ty_of_pty tyl)
in
let convert = function
| PMAty (PTyapp (q,[]))
-> MAts (find_ts th q)
| PMAty ty -> MAty (ty_of_pty ty)
| PMAfs q -> MAls (find_fs th q)
| PMAps q -> MAls (find_ps th q)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment