X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.ml;h=37a4f713688a21ac4bcbf65082466b190d10c2a9;hb=36f16f9b183c7324d8c8ff4851c6481a48296304;hp=22bdd0a4f5b78fac9d0146093bd70516b2ed3add;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index 22bdd0a4f..37a4f7136 100644
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/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         ->