Module Constrintern

type var_internalization_type =
| Inductive
| Recursive
| Method
| Variable
type var_internalization_data

This 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.t

A map of free variables to their implicit arguments and scopes

val empty_internalization_env : internalization_env
val compute_internalization_data : Environ.env -> Evd.evar_map -> Names.Id.t -> var_internalization_type -> EConstr.types -> Impargs.manual_implicits -> var_internalization_data
val 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_env
val 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_constr
val intern_type : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Glob_term.glob_constr
val 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_constr
val intern_pattern : Environ.env -> Constrexpr.cases_pattern_expr -> Names.lident list * (Names.Id.t Names.Id.Map.t * Glob_term.cases_pattern) list
val 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_context
val interp_casted_constr : Environ.env -> Evd.evar_map -> ?⁠impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> EConstr.constr Evd.in_evar_universe_context
val 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.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 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_pattern

Without typing

val interp_constr_pattern : Environ.env -> Evd.evar_map -> ?⁠expected_type:Pretyping.typing_constraint -> Constrexpr.constr_pattern_expr -> Pattern.constr_pattern

With typing

val intern_reference : Libnames.qualid -> Names.GlobRef.t option

Returns 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) option

Returns None if not a reference or a syndef not bound to a name

val interp_reference : ltac_sign -> Libnames.qualid -> Glob_term.glob_constr

Expands 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_context
val 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 option
val is_global : Names.Id.t -> bool
val 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_status

Interprets 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_constr
val parsing_explicit : bool Stdlib.ref

Globalization options

val for_grammar : ('a -> 'b) -> 'a -> 'b

Globalization leak for Grammar

val get_asymmetric_patterns : unit -> bool

Placeholder for global option, should be moved to a parameter

val check_duplicate : ?⁠loc:Loc.t -> (Libnames.qualid * Constrexpr.constr_expr) list -> unit

Check that a list of record field definitions doesn't contain duplicates.

val interp_known_level : Evd.evar_map -> Constrexpr.sort_name_expr -> Univ.Level.t
val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> Evd.evar_map * UState.universe_decl

Local universe and constraint declarations.

val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> Evd.evar_map * UState.universe_decl
val interp_cumul_univ_decl_opt : Environ.env -> Constrexpr.cumul_univ_decl_expr option -> Evd.evar_map * UState.universe_decl * Entries.variance_entry

BEWARE the variance entry needs to be adjusted by ComInductive.variance_of_entry if the instance is extensible.