package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.1.tar.gz

md5=13d2793fc6413aac5168822313e4864e

sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

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
53
54
55
56
57
58
59
60
61
(* generated by dune *)

(** @canonical Ltac2_plugin.G_ltac2 *)
module G_ltac2 = Ltac2_plugin__G_ltac2

(** @canonical Ltac2_plugin.Tac2bt *)
module Tac2bt = Ltac2_plugin__Tac2bt

(** @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.Tac2externals *)
module Tac2externals = Ltac2_plugin__Tac2externals

(** @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

(** @canonical Ltac2_plugin.Tac2typing_env *)
module Tac2typing_env = Ltac2_plugin__Tac2typing_env

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/ltac2_plugin/ltac2_plugin.ml.html

Source file ltac2_plugin.ml

Source file `ltac2_plugin.ml`