-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)
- | _ :: tl -> get_local f (succ i) tl
- in
- let get_global f =
- try
- let args = H.find st.henv gref in f (Some args)
- with Not_found -> f None
- in
- let g = function
- | Some args -> f gref (Some (Global args))
- | None -> f gref None
- in
- let f = function
- | Some i -> f gref (Some (Local i))
- | None -> get_global g
- in
- 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 false lenv) gref
- | Some resolved -> f gref resolved
+let resolve_lref f st l lenv id =
+ let rec aux f i = function
+ | [] -> f None
+ | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i)))
+ | _ :: tl -> aux f (succ i) tl
+ in
+ aux f 0 lenv
+
+let resolve_lref_strict f st l lenv id =
+ let f = function
+ | Some t -> f t
+ | None -> assert false