package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type var_internalization_type =
  1. | Inductive
  2. | Recursive
  3. | Method
  4. | Variable
type var_internalization_data
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 interp_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
val interp_casted_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * EConstr.constr
val interp_type_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.types
val interp_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)
val interp_casted_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)
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 locate_reference : Libnames.qualid -> Names.GlobRef.t
val is_global : Names.Id.t -> bool
val parsing_explicit : bool ref
val for_grammar : ('a -> 'b) -> 'a -> 'b
val get_asymmetric_patterns : unit -> bool
val check_duplicate : ?loc:Loc.t -> (Libnames.qualid * Constrexpr.constr_expr) list -> unit
val interp_known_level : Evd.evar_map -> Constrexpr.sort_name_expr -> Univ.Level.t