package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Implementation of Ltac-specific code to be exported in mlg files.

This is voluntarily undocumented. Please do not use in plugin code.

Tactics
val discrHyp : Names.Id.t -> unit Proofview.tactic
val injHyp : Names.Id.t -> unit Proofview.tactic
val refine_tac : Tacinterp.interp_sign -> simple:bool -> with_classes:bool -> Ltac_pretype.closed_glob_constr -> unit Proofview.tactic
val hResolve : Names.Id.t -> EConstr.t -> int -> EConstr.t -> unit Proofview.tactic
val hResolve_auto : Names.Id.t -> EConstr.t -> EConstr.t -> unit Proofview.tactic
val destauto : unit Proofview.tactic
val destauto_in : Names.Id.t -> unit Proofview.tactic
val has_evar : EConstr.t -> unit Proofview.tactic
val is_evar : EConstr.t -> unit Proofview.tactic
val is_var : EConstr.t -> unit Proofview.tactic
val is_fix : EConstr.t -> unit Proofview.tactic
val is_cofix : EConstr.t -> unit Proofview.tactic
val is_ind : EConstr.t -> unit Proofview.tactic
val is_constructor : EConstr.t -> unit Proofview.tactic
val is_proj : EConstr.t -> unit Proofview.tactic
val is_const : EConstr.t -> unit Proofview.tactic
val decompose : EConstr.t list -> EConstr.t -> unit Proofview.tactic
val tclOPTIMIZE_HEAP : unit Proofview.tactic
val onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic
Commands
val declare_equivalent_keys : Constrexpr.constr_expr -> Constrexpr.constr_expr -> unit
val infoH : pstate:Declare.Proof.t -> Tacexpr.raw_tactic_expr -> unit

ProofGeneral command

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct