package coq

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

Module Ltac_plugin.InternalsSource

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

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

Tactics
Sourceval discrHyp : Names.Id.t -> unit Proofview.tactic
Sourceval injHyp : Names.Id.t -> unit Proofview.tactic
Sourceval refine_tac : Tacinterp.interp_sign -> simple:bool -> with_classes:bool -> Ltac_pretype.closed_glob_constr -> unit Proofview.tactic
Sourceval hResolve : Names.Id.t -> EConstr.t -> int -> EConstr.t -> unit Proofview.tactic
Sourceval hResolve_auto : Names.Id.t -> EConstr.t -> EConstr.t -> unit Proofview.tactic
Sourceval destauto : unit Proofview.tactic
Sourceval destauto_in : Names.Id.t -> unit Proofview.tactic
Sourceval has_evar : EConstr.t -> unit Proofview.tactic
Sourceval is_evar : EConstr.t -> unit Proofview.tactic
Sourceval is_var : EConstr.t -> unit Proofview.tactic
Sourceval is_fix : EConstr.t -> unit Proofview.tactic
Sourceval is_cofix : EConstr.t -> unit Proofview.tactic
Sourceval is_ind : EConstr.t -> unit Proofview.tactic
Sourceval is_constructor : EConstr.t -> unit Proofview.tactic
Sourceval is_proj : EConstr.t -> unit Proofview.tactic
Sourceval is_const : EConstr.t -> unit Proofview.tactic
Sourceval decompose : EConstr.t list -> EConstr.t -> unit Proofview.tactic
Sourceval tclOPTIMIZE_HEAP : unit Proofview.tactic
Sourceval onSomeWithHoles : ('a option -> unit Proofview.tactic) -> 'a Tactypes.delayed_open option -> unit Proofview.tactic
Commands
Sourceval declare_equivalent_keys : Constrexpr.constr_expr -> Constrexpr.constr_expr -> unit
Sourceval 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