Module ComFixpoint

Fixpoints and cofixpoints
val do_fixpoint : ontop:Proof_global.t option -> Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> Proof_global.t option
val do_cofixpoint : ontop:Proof_global.t option -> Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.cofixpoint_expr * Vernacexpr.decl_notation list) list -> Proof_global.t option
type structured_fixpoint_expr = {
fix_name : Names.Id.t;
fix_univs : Constrexpr.universe_decl_expr option;
fix_annot : Names.lident option;
fix_binders : Constrexpr.local_binder_expr list;
fix_body : Constrexpr.constr_expr option;
fix_type : Constrexpr.constr_expr;
}
val interp_recursive : program_mode:bool -> cofix:bool -> structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (Names.Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * (EConstr.rel_context * Impargs.manual_explicitation list * int option) list

Exported for Program

val extract_fixpoint_components : structonly:bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> structured_fixpoint_expr list * Vernacexpr.decl_notation list
val extract_cofixpoint_components : (Vernacexpr.cofixpoint_expr * Vernacexpr.decl_notation list) list -> structured_fixpoint_expr list * Vernacexpr.decl_notation list
type recursive_preentry = Names.Id.t list * Sorts.relevance list * Constr.constr option list * Constr.types list
val interp_fixpoint : cofix:bool -> structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list
val declare_fixpoint : ontop:Proof_global.t option -> Decl_kinds.locality -> Decl_kinds.polymorphic -> (recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list) -> Proof_global.lemma_possible_guards -> Vernacexpr.decl_notation list -> Proof_global.t option

Not used so far

val declare_cofixpoint : ontop:Proof_global.t option -> Decl_kinds.locality -> Decl_kinds.polymorphic -> (recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list) -> Vernacexpr.decl_notation list -> Proof_global.t option
val compute_possible_guardness_evidences : (('a, 'b) Context.Rel.pt * 'c * int option) -> int list

Very private function, do not use