X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.ml;h=b4e9a4e94dda77e472926710485393c45799811f;hb=115915f23df4f56832d68b2f6b5b80c5afe019fc;hp=cf7df2d58a197ca9895837e784aa0a94e4b47294;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

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