Module Ltac_plugin.Internals
Tactics
val mytclWithHoles : (Tactics.evars_flag -> EConstr.constr Tactypes.with_bindings Tactics.destruction_arg option -> unit Proofview.tactic) -> Tactics.evars_flag -> Tactypes.delayed_open_constr_with_bindings Tactics.destruction_arg -> unit Proofview.tacticval with_delayed_uconstr : Tacinterp.interp_sign -> Ltac_pretype.closed_glob_constr -> (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tacticval replace_in_clause_maybe_by : Tacinterp.interp_sign -> Ltac_pretype.closed_glob_constr -> EConstr.constr -> Locus.clause -> Tacinterp.Value.t option -> unit Proofview.tacticval replace_term : Geninterp.interp_sign -> bool option -> Ltac_pretype.closed_glob_constr -> Locus.clause -> unit Proofview.tacticval discrHyp : Names.Id.t -> unit Proofview.tacticval injHyp : Names.Id.t -> unit Proofview.tacticval refine_tac : Tacinterp.interp_sign -> simple:bool -> with_classes:bool -> Ltac_pretype.closed_glob_constr -> unit Proofview.tacticval hResolve : Names.Id.t -> EConstr.t -> int -> EConstr.t -> unit Proofview.tacticval hResolve_auto : Names.Id.t -> EConstr.t -> EConstr.t -> unit Proofview.tacticval destauto : unit Proofview.tacticval destauto_in : Names.Id.t -> unit Proofview.tacticval has_evar : EConstr.t -> unit Proofview.tacticval is_evar : EConstr.t -> unit Proofview.tacticval is_var : EConstr.t -> unit Proofview.tacticval is_fix : EConstr.t -> unit Proofview.tacticval is_cofix : EConstr.t -> unit Proofview.tacticval is_ind : EConstr.t -> unit Proofview.tacticval is_constructor : EConstr.t -> unit Proofview.tacticval is_proj : EConstr.t -> unit Proofview.tacticval is_const : EConstr.t -> unit Proofview.tacticval unshelve : Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tacticval decompose : EConstr.t list -> EConstr.t -> unit Proofview.tacticval tclOPTIMIZE_HEAP : unit Proofview.tacticval onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tacticval exact : Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> unit Proofview.tactic
Commands
val declare_equivalent_keys : Constrexpr.constr_expr -> Constrexpr.constr_expr -> unitval infoH : pstate:Declare.Proof.t -> Tacexpr.raw_tactic_expr -> unitProofGeneral command