(* 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