Merge PR #10263: [proofs] Remove unused API [detected by coverage]

Ack-by: SkySkimmer
Reviewed-by: ppedrot

6 files changed, 0 insertions, 103 deletions

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 4a9404aa96..8439156e65 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -116,9 +116,6 @@ let lift c =
 
 let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
 
-let refine_one ~typecheck f =
-  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
-
 let refine ~typecheck f =
   let f evd =
     let (evd,c) = f evd in (evd,((), c))
diff --git a/proofs/refine.mli b/proofs/refine.mli
index b8948a92f3..93fd9d7a64 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni
     raised during the interpretation of [t] are caught and result in
     tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 
-val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
-(** A variant of [refine] which assumes exactly one goal under focus *)
-
 val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 799f4a380b..557f428be9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
 let tclTHEN_i tac taci gls =
   finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
 
-let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci
-let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
-
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
 let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
@@ -253,46 +250,9 @@ let rec tclFIRST = function
   | [] -> tclFAIL_s "No applicable tactic."
   |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
-let ite_gen tcal tac_if continue tac_else gl=
-  let success=ref false in
-  let tac_if0 gl=
-    let result=tac_if gl in
-      success:=true;result in
-  let tac_else0 e gl=
-    if !success then
-      iraise e
-    else
-      try
-        tac_else gl
-      with
-        e' when CErrors.noncritical e' -> iraise e in
-  try
-    tcal tac_if0 continue gl
-  with (* Breakpoint *)
-  | e when CErrors.noncritical e ->
-    let e = CErrors.push e in catch_failerror e; tac_else0 e gl
-
-(* Try the first tactic and, if it succeeds, continue with
-   the second one, and if it fails, use the third one *)
-
-let tclIFTHENELSE=ite_gen tclTHEN
-
-(* Idem with tclTHENS and tclTHENSV *)
-
-let tclIFTHENSELSE=ite_gen tclTHENS
-
-let tclIFTHENSVELSE=ite_gen tclTHENSV
-
-let tclIFTHENTRYELSEMUST tac1 tac2 gl =
-  tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
-
 (* Fails if a tactic did not solve the goal *)
 let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
 
-(* Try the first that solves the current goal *)
-let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
-
-
 (* Iteration tacticals *)
 
 let tclDO n t =
@@ -311,22 +271,7 @@ let rec tclREPEAT t g =
 
 let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
-(* Repeat on the first subgoal (no failure if no more subgoal) *)
-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
-
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-
-let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx}
-
-(* Push universe context *)
-let tclPUSHCONTEXT rigid ctx tac gl = 
-  tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl
-
 let tclPUSHEVARUNIVCONTEXT ctx gl = 
   tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
-
-let tclPUSHCONSTRAINTS cst gl = 
-  tclEVARS (Evd.add_constraints (project gl) cst) gl
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 52cbf7658b..0f34a79c49 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
-val tclEVARUNIVCONTEXT : UState.t -> tactic
-
-val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
 val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
 
-val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic
 
 (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
@@ -86,16 +82,6 @@ val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
    [tac2] for the remaining last subgoals (previously called tclTHENST) *)
 val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
 
-(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
-   applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
-   unchanged the other subgoals *)
-val tclTHENLASTn    : tactic -> tactic array -> tactic
-
-(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
-   applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
-   unchanged the other subgoals (previously called [tclTHENSI]) *)
-val tclTHENFIRSTn   : tactic -> tactic array -> tactic
-
 (** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.t Lazy.t
 
@@ -106,9 +92,7 @@ val catch_failerror  : Exninfo.iexn -> unit
 val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
-val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
-val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
@@ -118,16 +102,3 @@ val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
-
-(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
-   if it succeeds, applies [tac2] to the resulting subgoals,
-   and if not applies [tac3] to the initial goal [gls] *)
-val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
-val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
-
-(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
-   has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
-   Equivalent to [(tac1;try tac2)||tac2] *)
-
-val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 93031c2202..d7b4f729cb 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -81,12 +81,10 @@ let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
-let pf_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
 let pf_const_value              = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))
 
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
-
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
 (* Pretty-printers *)
@@ -181,14 +179,7 @@ module New = struct
   let pf_hnf_type_of gl t =
     pf_whd_all gl (pf_get_type_of gl t)
 
-  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
-
-  let pf_undefined_evars gl =
-    let sigma = Proofview.Goal.sigma gl in
-    let ev = Proofview.Goal.goal gl in
-    let evi = Evd.find sigma ev in
-      Evarutil.filtered_undefined_evars_of_evar_info sigma evi
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 23e1e6f566..195be04986 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -64,7 +64,6 @@ val pf_unfoldn    : (occurrences * evaluable_global_reference) list
 
 val pf_const_value : Goal.goal sigma -> pconstant -> constr
 val pf_conv_x      : Goal.goal sigma -> constr -> constr -> bool
-val pf_conv_x_leq  : Goal.goal sigma -> constr -> constr -> bool
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : Goal.goal sigma -> Pp.t
@@ -109,11 +108,8 @@ module New : sig
   val pf_hnf_constr : Proofview.Goal.t -> constr -> types
   val pf_hnf_type_of : Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : Proofview.Goal.t -> constr -> constr
   val pf_compute : Proofview.Goal.t -> constr -> constr
 
   val pf_nf_evar : Proofview.Goal.t -> constr -> constr
 
-  (** Gathers the undefined evars of the given goal. *)
-  val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t
 end