+
+(* FG: **********************************************************************)
+
+let list_rev_map_filter f l =
+ let rec aux a = function
+ | [] -> a
+ | hd :: tl ->
+ begin match f hd with
+ | None -> aux a tl
+ | Some b -> aux (b :: a) tl
+ end
+ in
+ aux [] l
+
+let get_name context index =
+ try match List.nth context (pred index) with
+ | Some (Cic.Name name, _) -> Some name
+ | _ -> None
+ with Invalid_argument "List.nth" -> None
+
+let get_rel context name =
+ let rec aux i = function
+ | [] -> None
+ | Some (Cic.Name s, _) :: _ when s = name -> Some (Cic.Rel i)
+ | _ :: tl -> aux (succ i) tl
+ in
+ aux 1 context