aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/refine.ml3
-rw-r--r--proofs/refine.mli3
-rw-r--r--proofs/refiner.ml55
-rw-r--r--proofs/refiner.mli29
-rw-r--r--proofs/tacmach.ml9
-rw-r--r--proofs/tacmach.mli4
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tacticals.mli9
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 16:41:57 +0000