(* 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
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 ->