package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type proj_kind = {
  1. pk_name : Names.Name.t;
  2. pk_true_proj : bool;
  3. pk_canonical : bool;
}
type struc_typ = {
  1. s_CONST : Names.constructor;
  2. s_EXPECTEDPARAM : int;
  3. s_PROJKIND : proj_kind list;
  4. s_PROJ : Names.Constant.t option list;
}
val register_structure : struc_typ -> unit
val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ
val rebuild_structure : Environ.env -> struc_typ -> struc_typ
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 is_projection : Names.Constant.t -> bool
val register_primitive_projection : Names.Projection.Repr.t -> Names.Constant.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. | Proj_cs of Names.Projection.Repr.t
  3. | Prod_cs
  4. | Sort_cs of Sorts.family
  5. | Default_cs
type obj_typ = {
  1. o_ORIGIN : Names.GlobRef.t;
  2. o_DEF : Constr.constr;
  3. o_CTX : Univ.AUContext.t;
  4. o_INJ : int option;
  5. o_TABS : Constr.constr list;
  6. o_TPARAMS : Constr.constr list;
  7. o_NPARAMS : int;
  8. 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 : Environ.env -> (Names.GlobRef.t * cs_pattern) -> Constr.constr * obj_typ
val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit
val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
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
val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> cs