Module Constrintern
Translation from front abstract syntax of term to untyped terms (glob_constr)
type var_internalization_type=|Inductive of Names.Id.t list * bool|Recursive|Method|Variabletype var_internalization_data= var_internalization_type * Names.Id.t list * Impargs.implicit_status list * Notation_term.scope_name option listtype 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 -> var_internalization_type -> EConstr.types -> Impargs.manual_explicitation list -> 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_explicitation list list -> internalization_env
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 : bool -> Environ.env -> internalization_env -> Constrexpr.local_binder_expr list -> internalization_env * Glob_term.glob_decl list
Composing internalization with type inference (pretyping)
val interp_constr : 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 : 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 : ?program_mode:bool -> 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_patternval intern_reference : Libnames.qualid -> Names.GlobRef.tRaise Not_found if syndef not bound to a name and error if unexisting ref
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 -> ?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.tval is_global : Names.Id.t -> boolval construct_reference : ('c, 't) Context.Named.pt -> Names.Id.t -> Names.GlobRef.tval global_reference : Names.Id.t -> Names.GlobRef.tval global_reference_in_absolute_module : Names.DirPath.t -> Names.Id.t -> Names.GlobRef.tval 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