[proofs] Remove unused API [detected by coverage]

We remove unused parts of the API, almost all of them belonging to the
legacy engine. This was detected using coverage testing.

The list is provisional and should be subject to change, let's see
what CI says.

8 files changed, 0 insertions, 120 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
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 59fd8b37d6..81700986ea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -43,12 +43,8 @@ let tclTHENS         = Refiner.tclTHENS
 let tclTHENSV        = Refiner.tclTHENSV
 let tclTHENSFIRSTn   = Refiner.tclTHENSFIRSTn
 let tclTHENSLASTn    = Refiner.tclTHENSLASTn
-let tclTHENFIRSTn    = Refiner.tclTHENFIRSTn
-let tclTHENLASTn     = Refiner.tclTHENLASTn
 let tclREPEAT        = Refiner.tclREPEAT
-let tclREPEAT_MAIN   = Refiner.tclREPEAT_MAIN
 let tclFIRST         = Refiner.tclFIRST
-let tclSOLVE         = Refiner.tclSOLVE
 let tclTRY           = Refiner.tclTRY
 let tclCOMPLETE      = Refiner.tclCOMPLETE
 let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
@@ -58,10 +54,6 @@ let tclDO            = Refiner.tclDO
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclSHOWHYPS      = Refiner.tclSHOWHYPS
 let tclTHENTRY       = Refiner.tclTHENTRY
-let tclIFTHENELSE    = Refiner.tclIFTHENELSE
-let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
-let tclIFTHENSVELSE   = Refiner.tclIFTHENSVELSE
-let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
 
 (************************************************************************)
 (* Tacticals applying on hypotheses                                     *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 201b7801c3..a9ccda527f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -31,13 +31,9 @@ val tclTHENLAST      : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENSV        : tactic -> tactic array -> tactic
 val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
-val tclTHENLASTn     : tactic -> tactic array -> tactic
 val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
-val tclTHENFIRSTn    : tactic -> tactic array -> 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 tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
@@ -49,11 +45,6 @@ val tclSHOWHYPS      : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
-val tclIFTHENELSE        : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE       : tactic -> tactic list -> tactic -> tactic
-val tclIFTHENSVELSE      : tactic -> tactic array -> tactic -> tactic
-val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
-
 (** {6 Tacticals applying to hypotheses } *)
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic