package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type var_internalization_type =
  1. | Inductive of Names.Id.t list * bool
  2. | Recursive
  3. | Method
  4. | Variable
type var_internalization_data = var_internalization_type * Names.Id.t list * Impargs.implicit_status list * Notation_term.scope_name option list
type internalization_env = var_internalization_data Names.Id.Map.t
val empty_internalization_env : internalization_env
type ltac_sign = {
  1. ltac_vars : Names.Id.Set.t;
  2. ltac_bound : Names.Id.Set.t;
  3. ltac_extra : Genintern.Store.t;
}
val empty_ltac_sign : ltac_sign
val intern_constr_pattern : Environ.env -> Evd.evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> Constrexpr.constr_pattern_expr -> Pattern.patvar list * Pattern.constr_pattern
val intern_reference : Libnames.qualid -> Names.GlobRef.t
val interp_reference : ltac_sign -> Libnames.qualid -> Glob_term.glob_constr
val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Evd.evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
val locate_reference : Libnames.qualid -> Names.GlobRef.t
val is_global : Names.Id.t -> bool
val construct_reference : ('c, 't) Context.Named.pt -> Names.Id.t -> Names.GlobRef.t
val global_reference : Names.Id.t -> Names.GlobRef.t
val global_reference_in_absolute_module : Names.DirPath.t -> Names.Id.t -> Names.GlobRef.t
val parsing_explicit : bool ref
val for_grammar : ('a -> 'b) -> 'a -> 'b
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