X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=6e7b5a8e74aa90deb24642ad3184f562233b18fb;hb=d18bffef7df9bbfc5ceae7ac7b607c96611e1978;hp=c3e6f04aa8286d56c8aa31bc5129eb99edbfd346;hpb=e31bb143e3a303321e509f415764338849b7e516;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index c3e6f04aa..6e7b5a8e7 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -705,3 +705,11 @@ let get_name context index =
       | 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