package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_sort : Sorts.t -> Pp.t
val pr_sort_family : Sorts.family -> Pp.t
val pr_fix : ('a -> Pp.t) -> ('a, 'a) Constr.pfixpoint -> Pp.t
val push_rel_assum : (Names.Name.t * EConstr.types) -> Environ.env -> Environ.env
val push_rels_assum : (Names.Name.t * Constr.types) list -> Environ.env -> Environ.env
val push_named_rec_types : (Names.Name.t array * Constr.types array * 'a) -> Environ.env -> Environ.env
val lookup_rel_id : Names.Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
val rel_vect : int -> int -> Constr.constr array
val rel_list : int -> int -> EConstr.constr list
val it_mkProd : EConstr.types -> (Names.Name.t * EConstr.types) list -> EConstr.types
val it_mkLambda : EConstr.constr -> (Names.Name.t * EConstr.types) list -> EConstr.constr
val it_mkProd_or_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkProd_wo_LetIn : EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val it_mkNamedProd_or_LetIn : EConstr.types -> EConstr.named_context -> EConstr.types
val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
val it_mkNamedLambda_or_LetIn : EConstr.constr -> EConstr.named_context -> EConstr.constr
val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
val map_constr_with_binders_left_to_right : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
val map_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> EConstr.constr) -> 'a -> EConstr.constr -> EConstr.constr
val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val fold_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> 'b -> EConstr.constr -> 'b) -> 'a -> 'b -> EConstr.constr -> 'b
val iter_constr_with_full_binders : Evd.evar_map -> (EConstr.rel_declaration -> 'a -> 'a) -> ('a -> EConstr.constr -> unit) -> 'a -> EConstr.constr -> unit
val strip_head_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
val drop_extra_implicit_args : Evd.evar_map -> EConstr.constr -> EConstr.constr
exception Occur
val occur_meta : Evd.evar_map -> EConstr.constr -> bool
val occur_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_meta_or_existential : Evd.evar_map -> EConstr.constr -> bool
val occur_metavariable : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
val occur_var_in_decl : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.named_declaration -> bool
val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool
val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t
val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val dependent_no_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val dependent_in_decl : Evd.evar_map -> EConstr.constr -> EConstr.named_declaration -> bool
val count_occurrences : Evd.evar_map -> EConstr.constr -> EConstr.constr -> int
val collect_metas : Evd.evar_map -> EConstr.constr -> int list
val collect_vars : Evd.evar_map -> EConstr.constr -> Names.Id.Set.t
val vars_of_global_reference : Environ.env -> Names.GlobRef.t -> Names.Id.Set.t
type meta_value_map = (Constr.metavariable * Constr.constr) list
val isMetaOf : Evd.evar_map -> Constr.metavariable -> EConstr.constr -> bool
type meta_type_map = (Constr.metavariable * Constr.types) list
val base_sort_cmp : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool
val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val eta_reduce_head : Evd.evar_map -> EConstr.constr -> EConstr.constr
val collapse_appl : Evd.evar_map -> EConstr.constr -> EConstr.constr
val prod_applist : Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val prod_applist_assum : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val strip_outer_cast : Evd.evar_map -> EConstr.constr -> EConstr.constr
exception CannotFilter
val decompose_prod_letin : Evd.evar_map -> EConstr.constr -> int * EConstr.rel_context * EConstr.constr
val nb_lam : Evd.evar_map -> EConstr.constr -> int
val nb_prod : Evd.evar_map -> EConstr.constr -> int
val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.constr -> int
val decompose_app_vect : Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr array
val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array
type names_context = Names.Name.t list
val lookup_name_of_rel : int -> names_context -> Names.Name.t
val lookup_rel_of_name : Names.Id.t -> names_context -> int
val empty_names_context : names_context
val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Names.Id.t list
val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list
val ids_of_context : Environ.env -> Names.Id.t list
val names_of_rel_context : Environ.env -> names_context
val env_rel_context_chop : int -> Environ.env -> Environ.env * EConstr.rel_context
val vars_of_env : Environ.env -> Names.Id.Set.t
val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Names.Name.t * 't) list
val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
val smash_rel_context : Constr.rel_context -> Constr.rel_context
val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
val fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a
val mem_named_context_val : Names.Id.t -> Environ.named_context_val -> bool
val compact_named_context : Constr.named_context -> Constr.compacted_context
val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
val clear_named_body : Names.Id.t -> Environ.env -> Environ.env
val global_vars : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.t list
val global_vars_set : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.Set.t
val global_vars_set_of_decl : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Names.Id.Set.t
val global_app_of_constr : Evd.evar_map -> EConstr.constr -> (Names.GlobRef.t * EConstr.EInstance.t) * EConstr.constr option
val dependency_closure : Environ.env -> Evd.evar_map -> EConstr.named_context -> Names.Id.Set.t -> Names.Id.t list
val is_section_variable : Names.Id.t -> bool
val is_global : Evd.evar_map -> Names.GlobRef.t -> EConstr.constr -> bool
val isGlobalRef : Evd.evar_map -> EConstr.constr -> bool
val is_template_polymorphic : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_Prop : Evd.evar_map -> EConstr.constr -> bool
val is_Set : Evd.evar_map -> EConstr.constr -> bool
val is_Type : Evd.evar_map -> EConstr.constr -> bool
val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
val on_judgment : ('a -> 'b) -> ('a, 'a) Environ.punsafe_judgment -> ('b, 'b) Environ.punsafe_judgment
val on_judgment_value : ('c -> 'c) -> ('c, 't) Environ.punsafe_judgment -> ('c, 't) Environ.punsafe_judgment
val on_judgment_type : ('t -> 't) -> ('c, 't) Environ.punsafe_judgment -> ('c, 't) Environ.punsafe_judgment
val pr_existential_key : Evd.evar_map -> Evar.t -> Pp.t
val pr_evar_suggested_name : Evar.t -> Evd.evar_map -> Names.Id.t
val pr_evar_info : Evd.evar_info -> Pp.t
val pr_evar_constraints : Evd.evar_map -> Evd.evar_constraint list -> Pp.t
val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.t
val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> Evd.evar_info -> bool) -> Evd.evar_map -> Pp.t
val pr_metaset : Evd.Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : Evd.evar_map -> Univ.Level.t -> Pp.t
module Internal : sig ... end
val print_constr : EConstr.constr -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead
val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead
val print_rel_context : Environ.env -> Pp.t
  • deprecated This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead