package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
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