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

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

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index 22bdd0a4f5b78fac9d0146093bd70516b2ed3add..37a4f713688a21ac4bcbf65082466b190d10c2a9 100644 (file)
--- a/components/tactics/eliminationTactics.ml
+++ b/components/tactics/eliminationTactics.ml
@@ -35,12 +35,6 @@ module H = ProofEngineHelpers
 
 (* unexported tactics *******************************************************)
 
-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 rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
@@ -48,7 +42,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
-         match get_name context index with 
+         match H.get_name context index with 
            | _ when index <= 0 -> (proof, [goal])
            | None              -> aux (pred index)
            | Some what         ->