Up – Package index » coq-core » Library coq-core.vernac » ComProgramFixpoint

Module `ComProgramFixpoint`Source

val 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.t

Special Fixpoint handling when command is activated.

Source

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