package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type struc_typ = {
  1. s_CONST : Names.constructor;
  2. s_EXPECTEDPARAM : int;
  3. s_PROJKIND : (Names.Name.t * bool) list;
  4. s_PROJ : Names.Constant.t option list;
}
type struc_tuple = Names.inductive * Names.constructor * (Names.Name.t * bool) list * Names.Constant.t option list
val declare_structure : struc_tuple -> unit
val lookup_structure : Names.inductive -> struc_typ
val lookup_projections : Names.inductive -> Names.Constant.t option list
val find_projection_nparams : Names.GlobRef.t -> int
val find_projection : Names.GlobRef.t -> struc_typ
val declare_primitive_projection : Names.Projection.Repr.t -> unit
val is_primitive_projection : Names.Constant.t -> bool
val find_primitive_projection : Names.Constant.t -> Names.Projection.Repr.t option
type cs_pattern =
  1. | Const_cs of Names.GlobRef.t
  2. | Prod_cs
  3. | Sort_cs of Sorts.family
  4. | Default_cs
type obj_typ = {
  1. o_DEF : Constr.constr;
  2. o_CTX : Univ.AUContext.t;
  3. o_INJ : int option;
  4. o_TABS : Constr.constr list;
  5. o_TPARAMS : Constr.constr list;
  6. o_NPARAMS : int;
  7. o_TCOMPS : Constr.constr list;
}
val cs_pattern_of_constr : Environ.env -> Constr.constr -> cs_pattern * int option * Constr.constr list
val pr_cs_pattern : cs_pattern -> Pp.t
val lookup_canonical_conversion : (Names.GlobRef.t * cs_pattern) -> Constr.constr * obj_typ
val declare_canonical_structure : Names.GlobRef.t -> unit
val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit -> ((Names.GlobRef.t * cs_pattern) * obj_typ) list