-let rec exp_term e t out tab = match t with
- | B.Sort (a, l) ->
- let a =
- let err _ = a in
- let f s = Y.Name (s, true) :: a in
- H.string_of_sort err f l
- in
- let attrs = [X.position l; X.name a] in
- X.tag X.sort attrs out tab
- | B.LRef (a, i) ->
- let a =
- let err _ = a in
- let f n r = Y.Name (n, r) :: a in
- let _, _, a, b = B.get e i in
- Y.name err f a
- in
- let attrs = [X.position i; X.name a] in
- X.tag X.lref attrs out tab
- | B.GRef (a, n) ->
- let a = Y.Name (U.name_of_uri n, true) :: a in
- let attrs = [X.uri n; X.name a] in
- X.tag X.gref attrs out tab
- | B.Cast (a, u, t) ->
- let attrs = [] in
- X.tag X.cast attrs ~contents:(exp_term e u) out tab;
- exp_term e t out tab
- | B.Appl (a, v, t) ->
- let attrs = [] in
- X.tag X.appl attrs ~contents:(exp_term e v) out tab;
- exp_term e t out tab
- | B.Bind (a, b, t) ->
- let a = rename C.start e a in
- exp_bind e a b out tab;
- exp_term (B.push e B.empty a b) t out tab
-
-and exp_bind e a b out tab = match b with
- | B.Abst w ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.abst attrs ~contents:(exp_term e w) out tab
- | B.Abbr v ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.abbr attrs ~contents:(exp_term e v) out tab
- | B.Void ->
- let attrs = [X.name a; X.mark a] in
- X.tag X.void attrs out tab
-
-let export_term = exp_term B.empty