X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2FmetaAut.ml;h=6a45518b5bbf1210f5f46d6ffa620a66e000fc3e;hb=673c78501a9e71ac5f897d2ba78f3591de8db876;hp=dd6c4a6f689208e76a9c4dba771790aa6a664baa;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git

diff --git a/helm/software/lambda-delta/src/toplevel/metaAut.ml b/helm/software/lambda-delta/src/toplevel/metaAut.ml
index dd6c4a6f6..6a45518b5 100644
--- a/helm/software/lambda-delta/src/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/src/toplevel/metaAut.ml
@@ -10,10 +10,10 @@
       V_______________________________________________________________ *)
 
 module U = NUri
-module H = U.UriHash
+module K = U.UriHash
 module C = Cps
-module O = Options
-module Y = Entity
+module G = Options
+module E = Entity
 module M = Meta
 module A = Aut
 
@@ -35,9 +35,9 @@ type resolver = Local of int
 
 let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *)
 
-let henv = H.create henv_size (* optimized global environment *)
+let henv = K.create henv_size (* optimized global environment *)
 
-let hcnt = H.create hcnt_size (* optimized context *) 
+let hcnt = K.create hcnt_size (* optimized context *) 
 
 (* Internal functions *******************************************************)
 
@@ -89,7 +89,7 @@ let resolve_lref_strict f st l lenv id =
    resolve_lref f st l lenv id
 
 let resolve_gref f st qid =
-   try let args = H.find henv (uri_of_qid qid) in f qid (Some args)
+   try let args = K.find henv (uri_of_qid qid) in f qid (Some args)
    with Not_found -> f qid None
 
 let resolve_gref_relaxed f st qid =
@@ -103,7 +103,7 @@ let resolve_gref_relaxed f st qid =
 let get_pars f st = function
    | None              -> f [] None
    | Some qid as node ->
-      try let pars = H.find hcnt (uri_of_qid qid) in f pars None
+      try let pars = K.find hcnt (uri_of_qid qid) in f pars None
       with Not_found -> f [] (Some node)
 
 let get_pars_relaxed f st =
@@ -164,7 +164,7 @@ let xlate_entity err f st = function
       let f qid = 
          let f pars =
 	    let f ww = 
-	       H.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
+	       K.add hcnt (uri_of_qid qid) ((name, ww) :: pars);
 	       err {st with node = Some qid}
 	    in
             xlate_term f st pars w
@@ -176,10 +176,10 @@ let xlate_entity err f st = function
       let f pars = 
          let f qid = 
             let f ww =
-	       H.add henv (uri_of_qid qid) pars;
-	       let a = [Y.Mark st.line] in
+	       K.add henv (uri_of_qid qid) pars;
+	       let a = [E.Mark st.line] in
 	       let entry = pars, ww, None in
-	       let entity = a, uri_of_qid qid, Y.Abst entry in
+	       let entity = a, uri_of_qid qid, E.Abst entry in
 	       f {st with line = succ st.line} entity
 	    in
 	    xlate_term f st pars w
@@ -191,10 +191,10 @@ let xlate_entity err f st = function
       let f pars = 
          let f qid = 
             let f ww vv = 
-	       H.add henv (uri_of_qid qid) pars;
-	       let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in 
+	       K.add henv (uri_of_qid qid) pars;
+	       let a = E.Mark st.line :: if trans then [] else [E.Priv] in 
 	       let entry = pars, ww, Some vv in
-	       let entity = a, uri_of_qid qid, Y.Abbr entry in
+	       let entity = a, uri_of_qid qid, E.Abbr entry in
 	       f {st with line = succ st.line} entity
 	    in
 	    let f ww = xlate_term (f ww) st pars v in
@@ -207,12 +207,12 @@ let xlate_entity err f st = function
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   H.clear henv; H.clear hcnt; {
-   path = []; node = None; nodes = []; line = 1; cover = !O.cover
+   K.clear henv; K.clear hcnt; {
+   path = []; node = None; nodes = []; line = 1; cover = !G.cover
 }
 
 let refresh_status st = {st with
-  cover = !O.cover
+  cover = !G.cover
 }  
 
 let meta_of_aut = xlate_entity