Removing unused functions in Refiner.

5 files changed, 21 insertions, 83 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7e80b40e52..9a78a79fd0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -315,49 +315,6 @@ let rec tclREPEAT_MAIN t g =
   (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else
     tclIDTAC)) tclIDTAC) g
 
-(*s Tactics handling a list of goals. *)
-
-type tactic_list = (goal list sigma) -> (goal list sigma)
-
-(* Functions working on goal list for correct backtracking in Prolog *)
-
-let tclFIRSTLIST = tclFIRST
-let tclIDTAC_list gls = gls
-
-(* first_goal : goal list sigma -> goal sigma *)
-
-let first_goal gls =
-  let gl = gls.it and sig_0 = gls.sigma in
-  if List.is_empty gl then error "first_goal";
-  { it = List.hd gl; sigma = sig_0; }
-
-(* goal_goal_list : goal sigma -> goal list sigma *)
-
-let goal_goal_list gls =
-  let gl = gls.it and sig_0 = gls.sigma in 
-  { it = [gl]; sigma = sig_0; }
-
-(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
-
-let apply_tac_list tac glls =
-  let (sigr,lg) = unpackage glls in
-  match lg with
-  | (g1::rest) ->
-      let gl = apply_sig_tac sigr tac g1 in
-      repackage sigr (gl@rest)
-  | _ -> error "apply_tac_list"
-
-let then_tactic_list tacl1 tacl2 glls =
-  let glls1 = tacl1 glls in
-  let glls2 = tacl2 glls1 in
-  glls2
-
-(* Transform a tactic_list into a tactic *)
-
-let tactic_list_tactic tac gls =
-    let glres = tac (goal_goal_list gls) in
-    glres
-
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 012209410a..2ea8777256 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -133,19 +133,6 @@ val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
-(** {6 Tactics handling a list of goals. } *)
-
-type tactic_list = goal list sigma -> goal list sigma
-
-val tclFIRSTLIST       : tactic_list list -> tactic_list
-val tclIDTAC_list      : tactic_list
-val first_goal         : 'a list sigma -> 'a sigma
-val apply_tac_list     : tactic -> tactic_list
-val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
-val tactic_list_tactic : tactic_list -> tactic
-val goal_goal_list     : 'a sigma -> 'a list sigma
-
-
 (* Check that holes in arguments have been resolved *)
 (* spiwack: used in [tclWITHHOLES] both newer and older copy. *)
 val check_evars : Environ.env -> evar_map -> evar_map -> evar_map -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fbe201f1a3..72a1287ec9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -104,21 +104,6 @@ let pf_check_type gls c1 c2 =
 let pf_is_matching              = pf_apply ConstrMatching.is_matching_conv
 let pf_matches                  = pf_apply ConstrMatching.matches_conv
 
-(************************************)
-(* Tactics handling a list of goals *)
-(************************************)
-
-type tactic_list = Refiner.tactic_list 
-
-let first_goal         = first_goal
-let goal_goal_list     = goal_goal_list
-let apply_tac_list     = apply_tac_list
-let then_tactic_list   = then_tactic_list
-let tactic_list_tactic = tactic_list_tactic
-let tclFIRSTLIST       = tclFIRSTLIST
-let tclIDTAC_list      = tclIDTAC_list
-
-
 (********************************************)
 (* Definition of the most primitive tactics *)
 (********************************************)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 897073f36b..a840dd15aa 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -112,18 +112,6 @@ val thin_body        : Id.t list -> tactic
 val move_hyp         : bool -> Id.t -> Id.t move_location -> tactic
 val rename_hyp       : (Id.t*Id.t) list -> tactic
 
-(** {6 Tactics handling a list of goals. } *)
-
-type tactic_list = Refiner.tactic_list
-
-val first_goal         : 'a list sigma -> 'a sigma
-val goal_goal_list     : 'a sigma -> 'a list sigma
-val apply_tac_list     : tactic -> tactic_list
-val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
-val tactic_list_tactic : tactic_list -> tactic
-val tclFIRSTLIST       : tactic_list list -> tactic_list
-val tclIDTAC_list      : tactic_list
-
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
 val pr_glls   : goal list sigma -> Pp.std_ppcmds
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 21c5a88c7a..65f0307426 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -56,6 +56,27 @@ let registered_e_assumption gl =
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
 
+(*s Tactics handling a list of goals. *)
+
+type tactic_list = (goal list sigma) -> (goal list sigma)
+
+(* first_goal : goal list sigma -> goal sigma *)
+
+let first_goal gls =
+  let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
+  if List.is_empty gl then error "first_goal";
+  { Evd.it = List.hd gl; Evd.sigma = sig_0; }
+
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+let apply_tac_list tac glls =
+  let (sigr,lg) = unpackage glls in
+  match lg with
+  | (g1::rest) ->
+      let gl = apply_sig_tac sigr tac g1 in
+      repackage sigr (gl@rest)
+  | _ -> error "apply_tac_list"
+
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
   @ (List.map Tactics.Simple.eapply (List.map mkVar (pf_ids_of_hyps gl)))