package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module G_ltac2 : sig ... end
module Tac2bt : sig ... end
module Tac2core : sig ... end
module Tac2dyn : sig ... end

Dynamic arguments for Ltac2.

module Tac2entries : sig ... end
module Tac2env : sig ... end

Ltac2 global environment

module Tac2expr : sig ... end
module Tac2externals : sig ... end

Interface for defining external tactics via a high-level spec.

module Tac2extffi : sig ... end
module Tac2ffi : sig ... end
module Tac2intern : sig ... end
module Tac2interp : sig ... end
module Tac2match : sig ... end

This file extends Matching with the main logic for Ltac2 match goal.

module Tac2print : sig ... end
module Tac2qexpr : sig ... end

Quoted variants of Ltac syntactic categories. Contrarily to the former, they sometimes allow anti-quotations. Used for notation scopes.

module Tac2quote : sig ... end

Syntactic quoting of expressions.

module Tac2stdlib : sig ... end

Standard tactics sharing their implementation with Ltac1

module Tac2tactics : sig ... end

Local reimplementations of tactics variants from Coq

module Tac2types : sig ... end

Redefinition of Ltac1 data structures because of impedance mismatch

module Tac2typing_env : sig ... end
module Tac2val : 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