Declarative language ported to new auto (with Universes).

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index c3e6f04aa8286d56c8aa31bc5129eb99edbfd346..b4e9a4e94dda77e472926710485393c45799811f 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -689,19 +689,16 @@ let lookup_type metasenv context hyp =
 
 (* 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