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