package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module ComRewrite : sig ... end
module Coretactics : sig ... end
module Extraargs : sig ... end
module Extratactics : sig ... end
module G_auto : sig ... end
module G_class : sig ... end
module G_eqdecide : sig ... end
module G_ltac : sig ... end
module G_obligations : sig ... end
module G_rewrite : sig ... end
module G_tactic : sig ... end
module Internals : sig ... end

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

module Leminv : sig ... end
module Pltac : sig ... end

Ltac parsing entries

module Pptactic : sig ... end

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

module Profile_ltac : sig ... end

Ltac profiling primitives

module Profile_ltac_tactics : sig ... end
module Tacarg : sig ... end
module 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.

module Tacentries : sig ... end

Ltac toplevel command entries.

module Tacenv : sig ... end

This module centralizes the various ways of registering tactics.

module Tacexpr : sig ... end
module Tacintern : sig ... end

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

module Tacinterp : sig ... end
module Tacsubst : sig ... end

Substitution of tactics at module closing time

module Tactic_debug : sig ... end

TODO: Move those definitions somewhere sensible

module Tactic_matching : sig ... end

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

module 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