ComProgramFixpoint (coq-core.ComProgramFixpoint)

val do_fixpoint : 
  pm:Declare.OblState.t ->
  scope:Locality.definition_scope ->
  ?clearbody:bool ->
  poly:bool ->
  ?typing_flags:Declarations.typing_flags ->
  ?deprecation:Deprecation.t ->
  ?using:Vernacexpr.section_subset_expr ->
  Vernacexpr.fixpoint_expr list ->
  Declare.OblState.t

Special Fixpoint handling when command is activated.

val do_cofixpoint : 
  pm:Declare.OblState.t ->
  scope:Locality.definition_scope ->
  poly:bool ->
  ?deprecation:Deprecation.t ->
  ?using:Vernacexpr.section_subset_expr ->
  Vernacexpr.cofixpoint_expr list ->
  Declare.OblState.t