package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/src/ltac_plugin/ltac_plugin.ml.html
Source file ltac_plugin.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85(* generated by dune *) (** @canonical Ltac_plugin.ComRewrite *) module ComRewrite = Ltac_plugin__ComRewrite (** @canonical Ltac_plugin.Coretactics *) module Coretactics = Ltac_plugin__Coretactics (** @canonical Ltac_plugin.Extraargs *) module Extraargs = Ltac_plugin__Extraargs (** @canonical Ltac_plugin.Extratactics *) module Extratactics = Ltac_plugin__Extratactics (** @canonical Ltac_plugin.G_auto *) module G_auto = Ltac_plugin__G_auto (** @canonical Ltac_plugin.G_class *) module G_class = Ltac_plugin__G_class (** @canonical Ltac_plugin.G_eqdecide *) module G_eqdecide = Ltac_plugin__G_eqdecide (** @canonical Ltac_plugin.G_ltac *) module G_ltac = Ltac_plugin__G_ltac (** @canonical Ltac_plugin.G_obligations *) module G_obligations = Ltac_plugin__G_obligations (** @canonical Ltac_plugin.G_rewrite *) module G_rewrite = Ltac_plugin__G_rewrite (** @canonical Ltac_plugin.G_tactic *) module G_tactic = Ltac_plugin__G_tactic (** @canonical Ltac_plugin.Internals *) module Internals = Ltac_plugin__Internals (** @canonical Ltac_plugin.Leminv *) module Leminv = Ltac_plugin__Leminv (** @canonical Ltac_plugin.Pltac *) module Pltac = Ltac_plugin__Pltac (** @canonical Ltac_plugin.Pptactic *) module Pptactic = Ltac_plugin__Pptactic (** @canonical Ltac_plugin.Profile_ltac *) module Profile_ltac = Ltac_plugin__Profile_ltac (** @canonical Ltac_plugin.Profile_ltac_tactics *) module Profile_ltac_tactics = Ltac_plugin__Profile_ltac_tactics (** @canonical Ltac_plugin.Tacarg *) module Tacarg = Ltac_plugin__Tacarg (** @canonical Ltac_plugin.Taccoerce *) module Taccoerce = Ltac_plugin__Taccoerce (** @canonical Ltac_plugin.Tacentries *) module Tacentries = Ltac_plugin__Tacentries (** @canonical Ltac_plugin.Tacenv *) module Tacenv = Ltac_plugin__Tacenv (** @canonical Ltac_plugin.Tacexpr *) module Tacexpr = Ltac_plugin__Tacexpr (** @canonical Ltac_plugin.Tacintern *) module Tacintern = Ltac_plugin__Tacintern (** @canonical Ltac_plugin.Tacinterp *) module Tacinterp = Ltac_plugin__Tacinterp (** @canonical Ltac_plugin.Tacsubst *) module Tacsubst = Ltac_plugin__Tacsubst (** @canonical Ltac_plugin.Tactic_debug *) module Tactic_debug = Ltac_plugin__Tactic_debug (** @canonical Ltac_plugin.Tactic_matching *) module Tactic_matching = Ltac_plugin__Tactic_matching (** @canonical Ltac_plugin.Tactic_option *) module Tactic_option = Ltac_plugin__Tactic_option