Merge the code paths for "CoFixpoint"/"Fixpoint" and "Theorem with"

[herbelin]

This is the eight part of #18811.

Main commit is "Sharing the code for "Theorem with" with the one for Fixpoint".

• Slight overlap with Apply the early check of the universe declaration and the monomorphic universe fixing to all interactive declarations #18960 to study (done)

Depends on:

• Adding a location to a few Fixpoint-related errors #19223 (minor dependency)
• Merging the code paths for Program Co/Fixpoint and Co/Fixpoint #19257
• Merge the execution paths for struct and measure/wf in Program Fixpoint #19258

[herbelin]

@coqbot run full ci

[Alizter]

Shouldn't these be **

[herbelin]

I don't think that odoc supports (** *) comments in between types. If I put (** I get this:
that is, it keeps only the last (** comment.

Generated with dune build @doc.

[Alizter]

Hmm I guess the correct way to do this would be in the comment attached to do_mutually_recrusive. You could write something like this:

(** [do_mutually_recursive ~program_mode ~poly recursives_exp] returns open obligations and open proofs if any. It takes the following arguents:
  - [program_ode] ...
  - [poly] ...
  - [recursives_exp] ...
  - [pm] is an optional argument that turns unresolved evars into obligations.
  - [use_interferene_hook] ...
 *)
val do_mutually_recursive
  :  ?pm:Declare.OblState.t
  -> program_mode:bool
  -> ?use_inference_hook:bool
  -> ?scope:Locality.definition_scope
  -> ?clearbody:bool
  -> poly:bool
  -> ?typing_flags:Declarations.typing_flags
  -> ?user_warns:UserWarn.t
  -> ?using:Vernacexpr.section_subset_expr
  -> recursives_expr
  -> Declare.OblState.t option * Declare.Proof.t option

The reason to do it this way is so that you can see how to use the function on hover. For instance, ocaml-lsp shows the odoc description of a function and having the full manual here can help without having to jump to the mli.

[Alizter]

As an example, here is the documentation of a variant in dune: https://github.com/ocaml/dune/blob/1e8b005dfe7d852887e0eb1d32e0260c9ef70d31/otherlibs/stdune/src/path.mli#L415-L422

[herbelin]

Somehow, I'm not convinced that it is where documentation is worth. These different functions (see e.g. also ComDefinition.do_definition) have the same arguments, 8 of them being actually components of a Declare.Info.t.

I feel that it would be better to properly document Declare.Info.t and to replace most of the arguments by an Info.t.

[ejgallego]

Maybe an opportunity to document and give this a better name?

[herbelin]

I don't know how to call it and I don't know either if it is worth to keep it.

[SkySkimmer]

@coqbot merge now