Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 3 insertions, 55 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5be9df317..5437d2ba1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -683,21 +683,3 @@ let prim_refiner r sigma goal =
 	(* Normalises evars in goals. Used by instantiate. *)
         let (goal,sigma) = Goal.V82.nf_evar sigma goal in
 	([goal],sigma)
-
-(************************************************************************)
-(************************************************************************)
-(* Extracting a proof term from the proof tree *)
-
-(* Util *)
-
-type variable_proof_status = ProofVar | SectionVar of identifier
-
-type proof_variable = name * variable_proof_status
-
-let proof_variable_index x =
-  let rec aux n = function
-    | (Name id,ProofVar)::l when x = id -> n
-    | _::l ->  aux (n+1) l
-    | [] -> raise Not_found
-  in
-  aux 1
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 696115a8a..75d9bd957 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -32,10 +32,6 @@ val with_check    : tactic -> tactic
 
 val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
-type proof_variable
-
-
-val proof_variable_index : identifier -> proof_variable list -> int
 
 (** {6 Refiner errors. } *)
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3dbb2190b..cad700b84 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -30,7 +30,7 @@ let undo n =
   let p = Proof_global.give_me_the_proof () in
   let d = Proof.V82.depth p in
   if n >= d then raise Proof.EmptyUndoStack;
-  for i = 1 to n do
+  for _i = 1 to n do
     Proof.undo p
   done
 
@@ -47,10 +47,6 @@ let undo_todepth n =
     undo ((current_proof_depth ()) - n )
   with Proof_global.NoCurrentProof  when n=0 -> ()
 
-let set_undo _ = ()
-let get_undo _ = None
-
-
 let start_proof id str hyps c ?init_tac ?compute_guard hook = 
   let goals = [ (Global.env_of_context hyps , c) ] in
   let init_tac = Option.map Proofview.V82.tactic init_tac in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index a421ccd0b..71afae020 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -29,8 +29,6 @@
      Therefore the undo stack stores action to be ran to undo.
 *)
 
-open Term
-
 type _focus_kind = int
 type 'a focus_kind = _focus_kind
 type focus_info = Obj.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bedf058fc..178c2ab2d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -314,8 +314,6 @@ let maximal_unfocus k p =
 
 module Bullet = struct
 
-
-
   type t = Vernacexpr.bullet
 
   type behavior = {
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 4a404b6f3..1f5ef315b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -11,7 +11,6 @@ open Evd
 open Names
 open Term
 open Tacexpr
-(* open Decl_expr *)
 open Glob_term
 open Genarg
 open Nametab
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 79b5ae731..98e1acc42 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -372,7 +372,7 @@ let list_of_sensitive s k env =
   with e when catchable_exception e ->
     tclZERO e env
 
-let tclGOALBIND s k = 
+let tclGOALBIND s k =
   (* spiwack: the first line ensures that the value returned by the tactic [k] will
       not "escape its scope". *)
   let k a = tclBIND (k a) here_s in
@@ -380,7 +380,7 @@ let tclGOALBIND s k =
     tclDISPATCHGEN Goal.null Goal.plus tacs
   end
 
-let tclGOALBINDU s k = 
+let tclGOALBINDU s k =
   tclBIND (list_of_sensitive s k) begin fun tacs ->
     tclDISPATCHGEN () unitK tacs
   end
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ac8de601e..4f75ffa52 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -117,9 +117,6 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
 let thensf_tac taci tac = thens3parts_tac taci tac [||]
 
-(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *)
-let thensl_tac tac taci = thens3parts_tac [||] tac taci
-
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
 let thensi_tac tac (sigr,gs) =
   let gll =
@@ -128,22 +125,6 @@ let thensi_tac tac (sigr,gs) =
 
 let then_tac tac = thensf_tac [||] tac
 
-let non_existent_goal n =
-  errorlabstrm ("No such goal: "^(string_of_int n))
-    (str"Trying to apply a tactic to a non existent goal")
-
-(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
-   the last goal (i=-1). *)
-let theni_tac i tac ((_,gl) as subgoals) =
-  let nsg = List.length gl in
-  let k = if i < 0 then nsg + i + 1 else i in
-  if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
-  else if k >= 1 & k <= nsg then
-    thensf_tac
-      (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
-      subgoals
-  else non_existent_goal k
-
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index cab124d93..4524fe6a1 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -109,8 +109,6 @@ let pf_matches                  = pf_apply Matching.matches_conv
 (* Tactics handling a list of goals *)
 (************************************)
 
-type transformation_tactic = proof_tree -> goal list 
-
 type validation_list = proof_tree list -> proof_tree list
 
 type tactic_list = Refiner.tactic_list