let f w = B.push "meta" f c l id (B.Abst w) in
xlate_term c f w
in
- C.list_fold_right f map pars B.empty_context
+ C.list_fold_right f map pars B.empty_lenv
let unwind_to_xlate_term f c t =
let map f t (l, id, b) = f (B.bind l id b t) in
let f t = C.list_fold_left f map t c in
xlate_term c f t
-let xlate_entry f = function
- | e, pars, uri, u, None ->
- let f u = f (e, uri, B.Abst u) in
+let xlate_entry f = function
+ | pars, u, None ->
let f c = unwind_to_xlate_term f c u in
xlate_pars f pars
- | e, pars, uri, u, Some (_, t) ->
- let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in
+ | pars, u, Some t ->
+ let f u t = f (B.Cast (u, t)) in
let f c u = unwind_to_xlate_term (f u) c t in
let f c = unwind_to_xlate_term (f c) c u in
xlate_pars f pars
-
-let xlate_item f = function
- | None -> f None
- | Some e -> let f e = f (Some e) in xlate_entry f e
-
+
(* Interface functions ******************************************************)
-let bag_of_meta = xlate_item
+let bag_of_meta = xlate_entry