Module `Genintern`Source

Sourcemodule Store : Store.S

Sourcetype intern_variable_status = {

intern_ids : Names.Id.Set.t;
notation_variable_status : (bool ref * Notation_term.subscopes option ref * Notation_term.notation_var_internalization_type) Names.Id.Map.t;

}

Sourcetype glob_sign = {

ltacvars : Names.Id.Set.t;
genv : Environ.env;
extra : Store.t;
intern_sign : intern_variable_status;

}

Sourceval empty_glob_sign : Environ.env -> glob_sign

Source

type glob_constr_and_expr =
  Glob_term.glob_constr * Constrexpr.constr_expr option

In globalize tactics, we need to keep the initial constr_expr to recompute in the environment by the effective calls to Intro, Inversion, etc The constr_expr field is None in TacDef though

Source

type glob_constr_pattern_and_expr =
  Names.Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern

Internalization functions

Sourcetype ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb

The type of functions used for internalizing generic arguments.

Sourceval intern : ('raw, 'glb, 'top) Genarg.genarg_type -> ('raw, 'glb) intern_fun

Source

val generic_intern : 
  (Genarg.raw_generic_argument, Genarg.glob_generic_argument) intern_fun

Substitution functions

Sourcetype 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb

The type of functions used for substituting generic arguments.

Sourceval substitute : ('raw, 'glb, 'top) Genarg.genarg_type -> 'glb subst_fun

Sourceval generic_substitute : Genarg.glob_generic_argument subst_fun

Notation functions

Sourcetype 'glb ntn_subst_fun = glob_constr_and_expr Names.Id.Map.t -> 'glb -> 'glb

Source

val substitute_notation : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  'glb ntn_subst_fun

Sourceval generic_substitute_notation : Genarg.glob_generic_argument ntn_subst_fun

Registering functions

Source

val register_intern0 : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  ('raw, 'glb) intern_fun ->
  unit

Source

val register_subst0 : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  'glb subst_fun ->
  unit

Source

val register_ntn_subst0 : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  'glb ntn_subst_fun ->
  unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Genintern/index.html

Module `Genintern`Source

Internalization functions

Substitution functions

Notation functions

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Genintern/index.html

Module GeninternSource

Internalization functions

Substitution functions

Notation functions

Module `Genintern`Source