- let g qid cnt =
- let map1 f = xlate_term f st lenv in
- let map2 f b =
- let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in
- D.name_of_binder C.err f b
- in
- let f tail =
- let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in
- let f cnt = C.list_rev_map_append f map2 cnt ~tail in
- C.list_sub_strict f cnt args
- in
- C.list_map f map1 args
+ let map1 f = function
+ | Y.Name (id, _) -> f (A.GRef ((id, true, []), []))
+ | _ -> C.err ()
+ in
+ let map2 f = xlate_term f st lenv in
+ let g qid (a, _) =
+ let gref = D.TGRef ([], uri_of_qid qid) in
+ match args with
+ | [] -> f gref
+ | args ->
+ let f args = f (D.TAppl ([], args, gref)) in
+ let f args = f (List.rev_map (map2 C.start) args) in
+ let f a = C.list_rev_map_append f map1 a ~tail:args in
+ C.list_sub_strict f a args