Module `Refiner`

Legacy proof engine. Do not use in newly written code.

type tactic = Proofview.V82.tac: The refiner (handles primitive rules and high-level tactics).

val tclIDTAC : tactic: tclIDTAC is the identity tactic without message printing

val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclEVARS : Evd.evar_map -> tactic: tclEVARS sigma changes the current evar map

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
val tclTHEN : tactic -> tactic -> tactic: tclTHEN tac1 tac2 gls applies the tactic tac1 to gls and applies tac2 to every resulting subgoals

val tclTHENLIST : tactic list -> tactic: tclTHENLIST [t1;..;tn] applies t1 THEN t2 ... THEN tn. More convenient than tclTHEN when n is large

val tclMAP : ('a -> tactic) -> 'a list -> tactic: tclMAP f [x1..xn] builds (f x1);(f x2);...(f xn)

val tclTHEN_i : tactic -> (int -> tactic) -> tactic: tclTHEN_i tac1 tac2 gls applies the tactic tac1 to gls and applies (tac2 i) to the i^th resulting subgoal (starting from 1)

val tclTHENLAST : tactic -> tactic -> tactic: tclTHENLAST tac1 tac2 gls applies the tactic tac1 to gls and tac2 to the last resulting subgoal (previously called tclTHENL)

val tclTHENFIRST : tactic -> tactic -> tactic: tclTHENFIRST tac1 tac2 gls applies the tactic tac1 to gls and tac2 to the first resulting subgoal

val tclTHENSV : tactic -> tactic array -> tactic: tclTHENS tac1 [|t1 ; ... ; tn|] gls applies the tactic tac1 to gls and applies t1,..., tn to the n resulting subgoals. Raises an error if the number of resulting subgoals is not n

val tclTHENS : tactic -> tactic list -> tactic: Same with a list of tactics

val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic: 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 subgoals and tac2 to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than n+m

val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic: tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls applies t1,...,tn on the last n resulting subgoals and tac2 on the remaining first subgoals

val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic: tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls first applies tac1, then applies t1,...,tn on the first n resulting subgoals and tac2 for the remaining last subgoals (previously called tclTHENST)

val tclTHENLASTn : tactic -> tactic array -> 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 tclTHENFIRSTn : 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)

exception FailError of int * Pp.t Stdlib.Lazy.t: A special exception for levels for the Fail tactic

val catch_failerror : Exninfo.iexn -> unit: Takes an exception and either raise it at the next level or do nothing.

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
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.t -> tactic
val tclFAIL_lazy : int -> Pp.t Stdlib.Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
val tclIFTHENELSE : tactic -> tactic -> 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