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 sig_it : 'a Evd.sigma -> 'a
val project : 'a Evd.sigma -> Evd.evar_map
val pf_env : Goal.goal Evd.sigma -> Environ.env
val pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context
val refiner : check:bool -> Constr.t -> tactic
Tacticals.
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 tclPUSHEVARUNIVCONTEXT : UState.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 ith 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)

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 tclFIRST : 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