package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.0.tar.gz

sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

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
86
87
88
(* generated by dune *)

(** @canonical Ltac_plugin.Coretactics *)
module Coretactics = Ltac_plugin__Coretactics

(** @canonical Ltac_plugin.Evar_tactics *)
module Evar_tactics = Ltac_plugin__Evar_tactics

(** @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.Rewrite *)
module Rewrite = Ltac_plugin__Rewrite

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

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/src/ltac_plugin/ltac_plugin.ml.html

Source file ltac_plugin.ml

Source file `ltac_plugin.ml`