level disambiguation cmpleted! the Grafite file is succesfully generated.

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index 2bfef6b0f458d37ead69e28cb4589b8f933599ec..fe562480d68db7be0d5721b55865eebe45f8310a 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -40,15 +40,20 @@ let hcnt = UH.create hcnt_size (* optimized context *)
 
 (* Internal functions *******************************************************)
 
-let empty_cnt = D.ESort
+let empty_cnt = D.empty_lenv
+
+let alpha id =
+   if id.[0] >= '0' && id.[0] <= '9' then !G.alpha ^ id else id
 
 let add_abst cnt id d w =
+   let id = if !G.alpha <> "" then alpha id else id in
    let a = E.node_attrs ~name:(id, true) ~degr:(succ d) () in 
    D.EBind (cnt, a, D.Abst (N.two, w)) 
 
 let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i))
 
-let id_of_name (id, _, _) = id
+let id_of_name (id, _, _) =
+   if !G.alpha <> "" then alpha id else id
 
 let mk_qid f lst id path =
    let str = String.concat "/" path in
@@ -117,6 +122,7 @@ let rec xlate_term f st lst y lenv = function
       let f _ vv = xlate_term (f vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
+      let name = if !G.alpha <> "" then alpha name else name in
       let f dw ww = 
          let a = E.node_attrs ~name:(name, true) () in
          let f dt tt =