- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / xml / xmlCrg.ml

diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml
index 2e10553cb25e3f76841387afbf2aeaae6d0afbc0..ec103f7ec93a7961a5d281bbc35e9c50625b6e52 100644 (file)
--- a/helm/software/helena/src/xml/xmlCrg.ml
+++ b/helm/software/helena/src/xml/xmlCrg.ml
@@ -19,24 +19,24 @@ module D  = Crg
 
 (* internal functions *******************************************************)
 
-let lenv_iter map_bind map_appl map_proj e lenv out tab = 
+let lenv_iter map_bind map_appl map_proj st e lenv out tab = 
    let rec aux = function
       | D.ESort           -> e
       | D.EBind (e, a, b) -> 
          let e = aux e in
 (* NOTE: the inner binders are alpha-converted first *)
          let a = R.alpha D.mem e a in
-         map_bind e a b out tab; D.EBind (e, a, b)
+         map_bind st e a b out tab; D.EBind (e, a, b)
       | D.EAppl (e, a, v) ->
          let e = aux e in
-         map_appl e a v out tab; D.EAppl (e, a, v)
+         map_appl st e a v out tab; D.EAppl (e, a, v)
       | D.EProj (e, a, d) ->
          let e = aux e in
-         map_proj e a d out tab; D.EProj (e, a, d)
+         map_proj st e a d out tab; D.EProj (e, a, d)
    in
    ignore (aux lenv)
 
-let rec exp_term e t out tab = match t with
+let rec exp_term st e t out tab = match t with
    | D.TSort (a, l)       ->
       let a =
          let err _ = a in
@@ -59,41 +59,41 @@ let rec exp_term e t out tab = match t with
       XL.tag XL.gref attrs out tab
    | D.TCast (a, u, t)    ->
       let attrs = [] in
-      XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
-      exp_term e t out tab
+      XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
+      exp_term st e t out tab
    | D.TAppl (a, v, t)    ->
       let attrs = [] in
-      XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
-      exp_term e t out tab
+      XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+      exp_term st e t out tab
    | D.TProj (a, lenv, t) ->
       let attrs = [] in
-      XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab;
-      exp_term (D.push_proj C.start a lenv e) t out tab
+      XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab;
+      exp_term st (D.push_proj C.start a lenv e) t out tab
    | D.TBind (a, b, t) ->
 (* NOTE: the inner binders are alpha-converted first *)
       let a = R.alpha D.mem e a in
-      exp_bind e a b out tab; 
-      exp_term (D.push_bind C.start a b e) t out tab 
+      exp_bind st e a b out tab; 
+      exp_term st (D.push_bind C.start a b e) t out tab 
 
-and exp_appl e a v out tab =
+and exp_appl st e a v out tab =
    let attrs = [] in
-   XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
+   XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
 
-and exp_bind e a b out tab = match b with
+and exp_bind st e a b out tab = match b with
    | D.Abst (n, w) ->
-      let attrs = [XL.level n; XL.name a] in
-      XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
+      let attrs = [XL.level st n; XL.name a] in
+      XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v      ->
       let attrs = [XL.name a] in
-      XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab
+      XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
    | D.Void        ->
       let attrs = [XL.name a] in
       XL.tag XL.void attrs out tab
 
-and exp_proj e a lenv out tab =
+and exp_proj st e a lenv out tab =
    let attrs = [] in
-   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab
+   XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab
 
 (* interface functions ******************************************************)
 
-let export_term = exp_term D.empty_lenv
+let export_term st = exp_term st D.empty_lenv