Module Constrintern
type var_internalization_type=|Inductive|Recursive|Method|Variabletype var_internalization_dataThis collects relevant information for interning local variables:
- their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable) e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive
- their implicit arguments
- their argument scopes
type internalization_env= var_internalization_data Names.Id.Map.tA map of free variables to their implicit arguments and scopes
val empty_internalization_env : internalization_envval compute_internalization_data : Environ.env -> Evd.evar_map -> Names.Id.t -> var_internalization_type -> EConstr.types -> Impargs.manual_implicits -> var_internalization_dataval compute_internalization_env : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> var_internalization_type -> Names.Id.t list -> EConstr.types list -> Impargs.manual_implicits list -> internalization_envval extend_internalization_data : var_internalization_data -> Impargs.implicit_status -> Notation_term.scope_name option -> var_internalization_data
type ltac_sign={ltac_vars : Names.Id.Set.t;Variables of Ltac which may be bound to a term
ltac_bound : Names.Id.Set.t;Other variables of Ltac
ltac_extra : Genintern.Store.t;Arbitrary payload
}
val empty_ltac_sign : ltac_sign
Internalization performs interpretation of global names and notations
val intern_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Glob_term.glob_constrval intern_type : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Glob_term.glob_constrval intern_gen : Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> Constrexpr.constr_expr -> Glob_term.glob_constrval intern_pattern : Environ.env -> Constrexpr.cases_pattern_expr -> Names.lident list * (Names.Id.t Names.Id.Map.t * Glob_term.cases_pattern) listval intern_context : Environ.env -> bound_univs:UnivNames.universe_binders -> internalization_env -> Constrexpr.local_binder_expr list -> internalization_env * Glob_term.glob_decl list
Composing internalization with type inference (pretyping)
val interp_constr : ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr Evd.in_evar_universe_contextval interp_casted_constr : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> EConstr.constr Evd.in_evar_universe_contextval interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types Evd.in_evar_universe_context
val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
val interp_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constrval interp_casted_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * EConstr.constrval 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 interp_type_evars_impls : ?flags:Pretyping.inference_flags -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * (EConstr.types * 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_patternWithout typing
val interp_constr_pattern : Environ.env -> Evd.evar_map -> ?expected_type:Pretyping.typing_constraint -> Constrexpr.constr_pattern_expr -> Pattern.constr_patternWith typing
val intern_reference : Libnames.qualid -> Names.GlobRef.t optionReturns None if it's a syndef not bound to a name, raises an error if not existing
val intern_name_alias : Constrexpr.constr_expr -> (Names.GlobRef.t * Glob_term.glob_level list option) optionReturns None if not a reference or a syndef not bound to a name
val interp_reference : ltac_sign -> Libnames.qualid -> Glob_term.glob_constrExpands abbreviations (syndef); raise an error if not existing
val interp_binder : Environ.env -> Evd.evar_map -> Names.Name.t -> Constrexpr.constr_expr -> EConstr.types Evd.in_evar_universe_contextval interp_binder_evars : Environ.env -> Evd.evar_map -> Names.Name.t -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.types
val interp_context_evars : ?program_mode:bool -> ?impl_env:internalization_env -> Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Evd.evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
val interp_named_context_evars : ?program_mode:bool -> ?impl_env:internalization_env -> Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Evd.evar_map * (internalization_env * ((Environ.env * EConstr.named_context) * Impargs.manual_implicits))
val locate_reference : Libnames.qualid -> Names.GlobRef.t optionval is_global : Names.Id.t -> boolval interp_notation_constr : Environ.env -> ?impls:internalization_env -> Notation_term.notation_interp_env -> Constrexpr.constr_expr -> (bool * Notation_term.subscopes) Names.Id.Map.t * Notation_term.notation_constr * Notation_term.reversibility_statusInterprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one.
val intern_core : Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> Genintern.intern_variable_status -> Constrexpr.constr_expr -> Glob_term.glob_constrval parsing_explicit : bool Stdlib.refGlobalization options
val get_asymmetric_patterns : unit -> boolPlaceholder for global option, should be moved to a parameter
val check_duplicate : ?loc:Loc.t -> (Libnames.qualid * Constrexpr.constr_expr) list -> unitCheck that a list of record field definitions doesn't contain duplicates.
val interp_known_level : Evd.evar_map -> Constrexpr.sort_name_expr -> Univ.Level.tval interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> Evd.evar_map * UState.universe_declLocal universe and constraint declarations.
val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> Evd.evar_map * UState.universe_declval interp_cumul_univ_decl_opt : Environ.env -> Constrexpr.cumul_univ_decl_expr option -> Evd.evar_map * UState.universe_decl * Entries.variance_entryBEWARE the variance entry needs to be adjusted by
ComInductive.variance_of_entryif the instance is extensible.