(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* metavariable val mk_new_meta : unit -> constr (* [new_untyped_evar] is a generator of unique evar keys *) val new_untyped_evar : unit -> existential_key (***********************************************************) (* Creating a fresh evar given their type and context *) val new_evar : evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr (* the same with side-effects *) val e_new_evar : evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr (* Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context [sign] and type [ty], [inst] is a mapping of the evar context to the context where the evar should occur. This means that the terms of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list (***********************************************************) (* Instantiate evars *) (* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way; failed if the instance is not valid for the given [ev] *) val evar_define : env -> existential -> constr -> evar_defs -> evar_defs (***********************************************************) (* Evars/Metas switching... *) (* [evars_to_metas] generates new metavariables for each non dependent existential and performs the replacement in the given constr; it also returns the evar_map extended with dependent evars *) val evars_to_metas : evar_map -> open_constr -> (evar_map * constr) val non_instantiated : evar_map -> (evar * evar_info) list (***********************************************************) (* Unification utils *) val is_ground_term : evar_defs -> constr -> bool val solve_refl : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) -> env -> evar_defs -> existential_key -> constr array -> constr array -> evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) -> env -> evar_defs -> conv_pb * existential * constr -> evar_defs * bool (* [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_defs -> constr -> unit val define_evar_as_product : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts val is_unification_pattern_evar : env -> existential -> constr list -> bool val is_unification_pattern : env -> constr -> constr array -> bool val solve_pattern_eqn : env -> constr list -> constr -> constr (***********************************************************) (* Value/Type constraints *) val judge_of_new_Type : unit -> unsafe_judgment type type_constraint_type = (int * int) option * constr type type_constraint = type_constraint_type option type val_constraint = constr option val empty_tycon : type_constraint val mk_tycon_type : constr -> type_constraint_type val mk_abstr_tycon_type : int -> constr -> type_constraint_type val mk_tycon : constr -> type_constraint val mk_abstr_tycon : int -> constr -> type_constraint val empty_valcon : val_constraint val mk_valcon : constr -> val_constraint val split_tycon : loc -> env -> evar_defs -> type_constraint -> evar_defs * (name * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type val lift_tycon_type : int -> type_constraint_type -> type_constraint_type val lift_tycon : int -> type_constraint -> type_constraint (***********************************************************) (* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) (* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *) val nf_evar : evar_map -> constr -> constr val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment val jl_nf_evar : evar_map -> unsafe_judgment list -> unsafe_judgment list val jv_nf_evar : evar_map -> unsafe_judgment array -> unsafe_judgment array val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment val nf_evar_info : evar_map -> evar_info -> evar_info val nf_evars : evar_map -> evar_map val nf_named_context_evar : evar_map -> named_context -> named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env (* Same for evar defs *) val nf_isevar : evar_defs -> constr -> constr val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment val jl_nf_isevar : evar_defs -> unsafe_judgment list -> unsafe_judgment list val jv_nf_isevar : evar_defs -> unsafe_judgment array -> unsafe_judgment array val tj_nf_isevar : evar_defs -> unsafe_type_judgment -> unsafe_type_judgment val nf_evar_defs : evar_defs -> evar_defs (* Replacing all evars *) exception Uninstantiated_evar of existential_key val whd_ise : evar_map -> constr -> constr val whd_castappevar : evar_map -> constr -> constr (* Replace the vars and rels that are aliases to other vars and rels by *) (* their representative that is most ancient in the context *) val expand_vars_in_term : env -> constr -> constr (*********************************************************************) (* debug pretty-printer: *) val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds val pr_tycon : env -> type_constraint -> Pp.std_ppcmds (**********************************) (* Removing hyps in evars'context *) val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types -> identifier list -> named_context_val * types