- X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv)
- | D.Bind (a, b, t) ->
- exp_lenv a b (exp_term t f)
-
-and exp_lenv a b f = match b with
- | D.Abst ws ->
- let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in
- X.tag X.abst attrs f ~contents:(list_iter exp_term ws)
- | D.Abbr vs ->
- let attrs = [X.name a; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs f ~contents:(list_iter exp_term vs)
- | D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs f
-
-let export_term = exp_term
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+ exp_term (D.push_proj C.start e a lenv) t out tab
+ | D.TBind (a, b, t) ->
+ exp_bind e a b out tab;
+ exp_term (D.push_bind C.start e a b) t out tab
+
+and exp_bind e a b out tab =
+ let f a ns = a, ns in
+ let a, ns = Y.get_names f a in
+ match b with
+ | D.Abst ws ->
+ let e = D.push_bind C.start e a (D.Abst []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+ X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+ | D.Abbr vs ->
+ let e = D.push_bind C.start e a (D.Abbr []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+ X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+ | D.Void n ->
+ let attrs = [X.name a; X.mark a; X.arity n] in
+ X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+let export_term = exp_term D.empty_lenv