package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac_pluginSource

Sourcemodule ComRewrite : sig ... end
Sourcemodule Coretactics : sig ... end
Sourcemodule Evar_tactics : sig ... end
Sourcemodule Extraargs : sig ... end
Sourcemodule Extratactics : sig ... end
Sourcemodule G_auto : sig ... end
Sourcemodule G_class : sig ... end
Sourcemodule G_eqdecide : sig ... end
Sourcemodule G_ltac : sig ... end
Sourcemodule G_obligations : sig ... end
Sourcemodule G_rewrite : sig ... end
Sourcemodule G_tactic : sig ... end
Sourcemodule Internals : sig ... end

Implementation of Ltac-specific code to be exported in mlg files.

Sourcemodule Leminv : sig ... end
Sourcemodule Pltac : sig ... end

Ltac parsing entries

Sourcemodule Pptactic : sig ... end

This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents.

Sourcemodule Profile_ltac : sig ... end

Ltac profiling primitives

Sourcemodule Profile_ltac_tactics : sig ... end

Ltac profiling entrypoints

Sourcemodule Tacarg : sig ... end
Sourcemodule Taccoerce : sig ... end

Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return something sensible according to the object content.

Sourcemodule Tacentries : sig ... end

Ltac toplevel command entries.

Sourcemodule Tacenv : sig ... end

This module centralizes the various ways of registering tactics.

Sourcemodule Tacexpr : sig ... end
Sourcemodule Tacintern : sig ... end

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

Sourcemodule Tacinterp : sig ... end
Sourcemodule Tacsubst : sig ... end

Substitution of tactics at module closing time

Sourcemodule Tactic_debug : sig ... end

TODO: Move those definitions somewhere sensible

Sourcemodule Tactic_matching : sig ... end

This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal.

Sourcemodule Tactic_option : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct