X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=5b85e46cbea703dd21fafe6f53b7242c6b5025b5;hb=625846fd7d1b0063b3b3a81ff9bbf36ddccf84f1;hp=52aa7314dfd2aa48c945b7769e8028be956da152;hpb=f4683c14c4b45e1844a4cfa91b706f41096ad98e;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 52aa7314d..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
 }
 
@@ -74,7 +75,7 @@ let relax_opt_qid f = function
    | None     -> f None
    | Some qid -> let f qid = f (Some qid) in relax_qid f qid
 
-let resolve_gref f st lenv gref =
+let resolve_gref f st local lenv gref =
   let rec get_local f i = function
      | []                                      -> f None
      | (name, _) :: _ when fst name = fst gref -> f (Some i)
@@ -93,14 +94,14 @@ let resolve_gref f st lenv gref =
       | Some i -> f gref (Some (Local i))
       | None   -> get_global g
   in
-  get_local f 0 lenv
+  if local then get_local f 0 lenv else f None
 
 let resolve_gref_relaxed f st lenv gref =
    let rec g gref = function
-      | None          -> relax_qid (resolve_gref g st lenv) gref
+      | None          -> relax_qid (resolve_gref g st false lenv) gref
       | Some resolved -> f gref resolved
    in
-   resolve_gref g st lenv gref
+   resolve_gref g st true lenv gref
 
 let get_pars f st = function
    | None              -> f [] None
@@ -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