package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val universes_context : Declarations.universes -> Univ.AUContext.t
val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) Declarations.declaration_arity -> ('c, 'd) Declarations.declaration_arity
val subst_const_body : Mod_subst.substitution -> Opaqueproof.opaque Declarations.constant_body -> Opaqueproof.opaque Declarations.constant_body
val constant_has_body : 'a Declarations.constant_body -> bool
val constant_polymorphic_context : 'a Declarations.constant_body -> Univ.AUContext.t
val constant_is_polymorphic : 'a Declarations.constant_body -> bool
val is_opaque : 'a Declarations.constant_body -> bool
val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
val pp_recarg : Declarations.recarg -> Pp.t
val pp_wf_paths : Declarations.wf_paths -> Pp.t
val mk_norec : Declarations.wf_paths
val dest_subterms : Declarations.wf_paths -> Declarations.wf_paths list array
val recarg_length : Declarations.wf_paths -> int -> int
val subst_mind_body : Mod_subst.substitution -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body
val inductive_polymorphic_context : Declarations.mutual_inductive_body -> Univ.AUContext.t
val inductive_is_polymorphic : Declarations.mutual_inductive_body -> bool
val inductive_is_cumulative : Declarations.mutual_inductive_body -> bool
val inductive_make_projection : Names.inductive -> Declarations.mutual_inductive_body -> proj_arg:int -> Names.Projection.Repr.t option
val inductive_make_projections : Names.inductive -> Declarations.mutual_inductive_body -> Names.Projection.Repr.t array option
val hcons_const_body : 'a Declarations.constant_body -> 'a Declarations.constant_body
val hcons_module_body : Declarations.module_body -> Declarations.module_body