ComProgramFixpointval do_fixpoint : pm:Declare.OblState.t -> scope:Locality.definition_scope -> poly:bool -> ?typing_flags:Declarations.typing_flags -> ?using:Vernacexpr.section_subset_expr -> Vernacexpr.fixpoint_expr list -> Declare.OblState.tSpecial Fixpoint handling when command is activated.
val do_cofixpoint : pm:Declare.OblState.t -> scope:Locality.definition_scope -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> Vernacexpr.cofixpoint_expr list -> Declare.OblState.t