package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val closedn : int -> Constr.constr -> bool
val closed0 : Constr.constr -> bool
val noccurn : int -> Constr.constr -> bool
val noccur_between : int -> int -> Constr.constr -> bool
val noccur_with_meta : int -> int -> Constr.constr -> bool
val liftn : int -> int -> Constr.constr -> Constr.constr
val lift : int -> Constr.constr -> Constr.constr
type substl = Constr.constr list
val subst_of_rel_context_instance : Constr.rel_context -> Constr.constr list -> substl
val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int
val substnl : substl -> int -> Constr.constr -> Constr.constr
val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration
val replace_vars : (Names.Id.t * Constr.constr) list -> Constr.constr -> Constr.constr
val substn_vars : int -> Names.Id.t list -> Constr.constr -> Constr.constr
val subst_vars : Names.Id.t list -> Constr.constr -> Constr.constr
val subst_var : Names.Id.t -> Constr.constr -> Constr.constr
val subst_univs_level_constr : Univ.universe_level_subst -> Constr.constr -> Constr.constr
val subst_instance_constr : Univ.Instance.t -> Constr.constr -> Constr.constr
val subst_instance_context : Univ.Instance.t -> Constr.rel_context -> Constr.rel_context
val universes_of_constr : Constr.constr -> Univ.LSet.t