X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=5b85e46cbea703dd21fafe6f53b7242c6b5025b5;hb=1b9751de891efa2761cdc6cb9d019df6aaaa8514;hp=370bf4cfd6cee01bfc68f5c1d78a8f9e248b5060;hpb=ac6e72ade957c5ad253362b149140f7f9fd5ec5d;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 370bf4cfd..5b85e46cb 100644
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -39,6 +39,7 @@ type status = {
    hcnt: environment;        (* optimized context *)   
    node: context_node;       (* current context node *)
    nodes: context_node list; (* context node list *)
+   line: int;                (* line number *)
    explicit: bool            (* need explicit context root? *)
 }
 
@@ -48,7 +49,7 @@ type resolver = Local of int
 let hsize = 11 (* hash tables initial size *)
 
 let initial_status size = {
-   genv = []; path = []; node = None; nodes = []; explicit = true;
+   genv = []; path = []; node = None; nodes = []; line = 1; explicit = true;
    henv = H.create size; hcnt = H.create size
 }
 
@@ -133,10 +134,11 @@ let rec xlate_term f st lenv = function
       let f name = function
 	 | Local i     -> f (M.LRef i)
          | Global defs -> 
-            let map1 f = xlate_term f st lenv in
-	    let map2 f (name, _) = f (M.GRef (name, [])) in
+            let l = List.length lenv in
+	    let map1 f = xlate_term f st lenv in
+	    let map2 f (name, _) = f (M.GRef (l, name, [])) in
             let f tail =  	   
-	       let f args = f (M.GRef (name, args)) in
+	       let f args = f (M.GRef (l, name, args)) in
                let f defs = Cps.list_rev_map_append f map2 defs ~tail in
 	       Cps.list_sub_strict f defs args
 	    in
@@ -175,9 +177,9 @@ let xlate_item f st = function
       let f pars = 
          let f name = 
             let f ww =
-	       let entry = (pars, name, ww, None) in
+	       let entry = (st.line, pars, name, ww, None) in
 	       H.add st.henv name pars;
-	       f {st with genv = entry :: st.genv}
+	       f {st with genv = entry :: st.genv; line = succ st.line}
 	    in
 	    xlate_term f st pars w
 	 in
@@ -188,9 +190,9 @@ let xlate_item f st = function
       let f pars = 
          let f name = 
             let f ww vv = 
-	       let entry = (pars, name, ww, Some (trans, vv)) in
+	       let entry = (st.line, pars, name, ww, Some (trans, vv)) in
 	       H.add st.henv name pars;
-	       f {st with genv = entry :: st.genv}
+	       f {st with genv = entry :: st.genv; line = succ st.line}
 	    in
 	    let f ww = xlate_term (f ww) st pars v in
 	    xlate_term f st pars w