package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

module Store : Store.S

type glob_sign = {

}

val empty_glob_sign : Environ.env -> glob_sign

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

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

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

type !'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb

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

val generic_substitute : Genarg.glob_generic_argument subst_fun

type !'glb ntn_subst_fun =
  Tactypes.glob_constr_and_expr Names.Id.Map.t ->
  'glb ->
  'glb

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

val generic_substitute_notation : Genarg.glob_generic_argument ntn_subst_fun

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

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

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