Unlocking the interface was not performed as the last action of the callback.

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

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index c3e6f04aa8286d56c8aa31bc5129eb99edbfd346..6e7b5a8e74aa90deb24642ad3184f562233b18fb 100644 (file)
--- 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