- "linear" flag added to lapply (automatic clearing)

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

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index cf7df2d58a197ca9895837e784aa0a94e4b47294..c3e6f04aa8286d56c8aa31bc5129eb99edbfd346 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -686,3 +686,22 @@ let lookup_type metasenv context hyp =
       | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
    in
    aux 1 context
+
+(* 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