- lambda-delta: some speed up (not very much :) actually)

[helm.git] / helm / software / lambda-delta / toplevel / metaAut.ml

diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml
index 52aa7314dfd2aa48c945b7769e8028be956da152..370bf4cfd6cee01bfc68f5c1d78a8f9e248b5060 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaAut.ml
+++ b/helm/software/lambda-delta/toplevel/metaAut.ml
@@ -74,7 +74,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 +93,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