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 -> Misctypes.patvar list * Pattern.constr_pattern
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 is_global : Names.Id.t -> bool
val construct_reference : ('c, 't) Context.Named.pt -> Names.Id.t -> Globnames.global_reference
val global_reference : Names.Id.t -> Globnames.global_reference
val global_reference_in_absolute_module : Names.DirPath.t -> Names.Id.t -> Globnames.global_reference
val parsing_explicit : bool Pervasives.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