Proofview: move [list_goto] to the [CList] module.

It is, after all, a generic function about lists.

4 files changed, 5 insertions, 34 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb826bedc4..b96a12c46d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -102,7 +102,7 @@ let solve ?with_end_tac gi tac pr =
     Proof.run_tactic (Global.env ()) tac pr
   with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
-    | Proofview.IndexOutOfRange ->
+    | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
 	                            Errors.errorlabstrm "" msg
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 15ce940115..24fdc41dac 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -215,7 +215,7 @@ let _unfocus pr =
    a need for it? *)
 let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
-  with Proofview.IndexOutOfRange -> raise (NoSuchGoals (i,i))
+  with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8272b17db7..860e29fffc 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -158,31 +158,6 @@ let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
 
-(* spiwack: this function should probably go in the Util section,
-    but I'd rather have Util (or a separate module for lists)
-    raise proper exceptions before *)
-(* [IndexOutOfRange] occurs in case of malformed indices
-   with respect to list lengths. *)
-exception IndexOutOfRange
-(* no handler: should not be allowed to reach toplevel *)
-
-(* [list_goto i l] returns a pair of lists [c,t] where
-   [c] has length [i] and is the reversed of the [i] first
-   elements of [l], and [t] is the rest of the list.
-   The idea is to navigate through the list, [c] is then
-   seen as the context of the current position. 
-   Raises [IndexOutOfRange] if [i > length l]*)
-let list_goto = 
-  let rec aux acc index = function
-    | l when Int.equal index 0-> (acc,l)
-    | [] -> raise IndexOutOfRange
-    | a::q -> aux (a::acc) (index-1) q
-  in
-  fun i l ->
-    if i < 0 then
-      raise IndexOutOfRange
-    else
-      aux [] i l
 
 (* Type of the object which allow to unfocus a view.*)
 (* First component is a reverse list of what comes before
@@ -202,10 +177,10 @@ let focus_context f = f
    [focus_sublist i j l] raises [IndexOutOfRange] if
    [i > length l], or [j > length l] or [ j < i ].  *)
 let focus_sublist i j l =
-  let (left,sub_right) = list_goto (i-1) l in
+  let (left,sub_right) = CList.goto (i-1) l in
   let (sub, right) = 
     try List.chop (j-i+1) sub_right
-    with Failure _ -> raise IndexOutOfRange
+    with Failure _ -> raise CList.IndexOutOfRange
   in
   (sub, (left,right))
 
@@ -409,7 +384,7 @@ let tclFOCUS_gen nosuchgoal i j t =
     t >>= fun result ->
     Pv.modify (fun next -> unfocus context next) >>
     Proof.ret result
-  with IndexOutOfRange -> nosuchgoal
+  with CList.IndexOutOfRange -> nosuchgoal
 
 let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
 let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0d9c64a5ce..b758d0aec4 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -61,10 +61,6 @@ val initial_goals : entry -> (constr * types) list
 
 (*** Focusing operations ***)
 
-(* [IndexOutOfRange] occurs in case of malformed indices
-   with respect to list lengths. *)
-exception IndexOutOfRange
-
 (* Type of the object which allow to unfocus a view.*)
 type focus_context