package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/src/ltac2_plugin/ltac2_plugin.ml.html
Source file ltac2_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(* generated by dune *) (** @canonical Ltac2_plugin.G_ltac2 *) module G_ltac2 = Ltac2_plugin__G_ltac2 (** @canonical Ltac2_plugin.Tac2core *) module Tac2core = Ltac2_plugin__Tac2core (** @canonical Ltac2_plugin.Tac2dyn *) module Tac2dyn = Ltac2_plugin__Tac2dyn (** @canonical Ltac2_plugin.Tac2entries *) module Tac2entries = Ltac2_plugin__Tac2entries (** @canonical Ltac2_plugin.Tac2env *) module Tac2env = Ltac2_plugin__Tac2env (** @canonical Ltac2_plugin.Tac2expr *) module Tac2expr = Ltac2_plugin__Tac2expr (** @canonical Ltac2_plugin.Tac2extffi *) module Tac2extffi = Ltac2_plugin__Tac2extffi (** @canonical Ltac2_plugin.Tac2ffi *) module Tac2ffi = Ltac2_plugin__Tac2ffi (** @canonical Ltac2_plugin.Tac2intern *) module Tac2intern = Ltac2_plugin__Tac2intern (** @canonical Ltac2_plugin.Tac2interp *) module Tac2interp = Ltac2_plugin__Tac2interp (** @canonical Ltac2_plugin.Tac2match *) module Tac2match = Ltac2_plugin__Tac2match (** @canonical Ltac2_plugin.Tac2print *) module Tac2print = Ltac2_plugin__Tac2print (** @canonical Ltac2_plugin.Tac2qexpr *) module Tac2qexpr = Ltac2_plugin__Tac2qexpr (** @canonical Ltac2_plugin.Tac2quote *) module Tac2quote = Ltac2_plugin__Tac2quote (** @canonical Ltac2_plugin.Tac2stdlib *) module Tac2stdlib = Ltac2_plugin__Tac2stdlib (** @canonical Ltac2_plugin.Tac2tactics *) module Tac2tactics = Ltac2_plugin__Tac2tactics (** @canonical Ltac2_plugin.Tac2types *) module Tac2types = Ltac2_plugin__Tac2types