package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/ltac2_plugin/Ltac2_plugin/Tac2env/index.html

Module Ltac2_plugin.Tac2envSource

Ltac2 global environment

Toplevel definition of values
Sourcetype global_data = {
  1. gdata_expr : Tac2expr.glb_tacexpr;
  2. gdata_type : Tac2expr.type_scheme;
  3. gdata_mutable : bool;
  4. gdata_deprecation : Deprecation.t option;
}
Sourceval define_global : Tac2expr.ltac_constant -> global_data -> unit
Sourcetype compile_info = {
  1. source : string;
}
Sourceval set_compiled_global : Tac2expr.ltac_constant -> compile_info -> Tac2val.valexpr -> unit
Sourceval get_compiled_global : Tac2expr.ltac_constant -> (compile_info * Tac2val.valexpr) option
Sourceval globals : unit -> global_data Names.KNmap.t
Toplevel definition of types
Toplevel definition of algebraic constructors
Sourcetype constructor_data = {
  1. cdata_prms : int;
    (*

    Type parameters

    *)
  2. cdata_type : Tac2expr.type_constant;
    (*

    Inductive definition to which the constructor pertains

    *)
  3. cdata_args : int Tac2expr.glb_typexpr list;
    (*

    Types of the constructor arguments

    *)
  4. cdata_indx : int option;
    (*

    Index of the constructor in the ADT. Numbering is duplicated between argumentless and argument-using constructors, e.g. in type 'a option None and Some have both index 0. This field is empty whenever the constructor is a member of an open type.

    *)
}
Sourceval define_constructor : Tac2expr.ltac_constructor -> constructor_data -> unit
Sourceval find_all_constructors_in_type : Tac2expr.type_constant -> constructor_data Names.KNmap.t

Useful for printing info about currently defined constructors of open types.

Toplevel definition of projections
Sourcetype projection_data = {
  1. pdata_prms : int;
    (*

    Type parameters

    *)
  2. pdata_type : Tac2expr.type_constant;
    (*

    Record definition to which the projection pertains

    *)
  3. pdata_ptyp : int Tac2expr.glb_typexpr;
    (*

    Type of the projection

    *)
  4. pdata_mutb : bool;
    (*

    Whether the field is mutable

    *)
  5. pdata_indx : int;
    (*

    Index of the projection

    *)
}
Sourceval define_projection : Tac2expr.ltac_projection -> projection_data -> unit
Toplevel definition of aliases
Sourcetype alias_data = {
  1. alias_body : Tac2expr.raw_tacexpr;
  2. alias_depr : Deprecation.t option;
}
Sourceval define_alias : ?deprecation:Deprecation.t -> Tac2expr.ltac_constant -> Tac2expr.raw_tacexpr -> unit
Toplevel definition of notations
Sourcetype notation_data =
  1. | UntypedNota of Tac2expr.raw_tacexpr
  2. | TypedNota of {
    1. nota_prms : int;
    2. nota_argtys : int Tac2expr.glb_typexpr Names.Id.Map.t;
    3. nota_ty : int Tac2expr.glb_typexpr;
    4. nota_body : Tac2expr.glb_tacexpr;
    }
Sourceval define_notation : Tac2expr.ltac_notation -> notation_data -> unit
Name management
Sourceval locate_extended_all_ltac : Libnames.qualid -> Tac2expr.tacref list
Sourceval shortest_qualid_of_ltac : Names.Id.Set.t -> Tac2expr.tacref -> Libnames.qualid
Sourceval locate_extended_all_constructor : Libnames.qualid -> Tac2expr.ltac_constructor list
Sourceval shortest_qualid_of_constructor : Tac2expr.ltac_constructor -> Libnames.qualid
Sourceval locate_extended_all_type : Libnames.qualid -> Tac2expr.type_constant list
Sourceval shortest_qualid_of_type : ?loc:Loc.t -> Tac2expr.type_constant -> Libnames.qualid
Sourceval locate_extended_all_projection : Libnames.qualid -> Tac2expr.ltac_projection list
Sourceval shortest_qualid_of_projection : Tac2expr.ltac_projection -> Libnames.qualid
Toplevel definitions of ML tactics

This state is not part of the summary, contrarily to the ones above. It is intended to be used from ML plugins to register ML-side functions.

Sourceval define_primitive : Tac2expr.ml_tactic_name -> Tac2val.valexpr -> unit
ML primitive types
Sourcetype 'a or_glb_tacexpr =
  1. | GlbVal of 'a
  2. | GlbTacexpr of Tac2expr.glb_tacexpr
Sourcetype ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r Tac2expr.glb_typexpr
Sourcetype environment = {
  1. env_ist : Tac2val.valexpr Names.Id.Map.t;
}
Sourcetype ('a, 'b) ml_object = {
  1. ml_intern : 'r. (Tac2expr.raw_tacexpr, Tac2expr.glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
  2. ml_subst : Mod_subst.substitution -> 'b -> 'b;
  3. ml_interp : environment -> 'b -> Tac2val.valexpr Proofview.tactic;
  4. ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
  5. ml_raw_print : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
}
Sourceval define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
Sourceval interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object
Absolute paths
Sourceval coq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

Sourceval std_prefix : Names.ModPath.t

Path where Ltac-specific datatypes are defined in Ltac2 plugin.

Sourceval ltac1_prefix : Names.ModPath.t

Path where the Ltac1 legacy FFI is defined.

Generic arguments

Ltac2 quotations in Ltac1 code

Ltac2 quotations in Ltac1 returning Ltac1 values. When ids are bound interning turns them into Ltac1.lambda.

Ltac2 quotations in Gallina terms

Sourcetype var_quotation_kind =
  1. | ConstrVar
  2. | PretermVar
  3. | PatternVar

Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms. NB: "$x" means "$constr:x"

Embedding Ltac2 closures of type Ltac1.t -> Ltac1.t inside Ltac1. There is no relevant data because arguments are passed by conventional names.

Helper functions
Sourceval is_constructor_id : Names.Id.t -> bool
Sourceval is_constructor : Libnames.qualid -> bool