Refine description of "About" and mention transparency.

[jfehrle]

I also edited the text describing the transparency states to make them match the description in the Strategy command. Let me know if I guessed wrong.

[SkySkimmer]

cc @herbelin

[jfehrle]

@coq/doc-maintainers Would someone review?

[herbelin]

Regarding the transparency message, I think it is ok as the PR does (this will be adapted anyway in #19029)

Regarding the "expansion weight" lines, which I don't know how it works, I have no idea whether the change is worth or not.

[jfehrle]

Regarding the "expansion weight" lines, which I don't know how it works, I have no idea whether the change is worth or not.

Does this help?

Conv_oracle fields used in prettyp.ml appear to be set by the parameters of the Strategy command. The description of that command made sense. "expansion weight" suggests something like w₁*item₁ + w₂*item₂ + ... +w_n*item_n, which is more complex than what the command description says. The command description uses "level", which seems a better fit than "weight" as well as "expand", which I used in the updated messages.

  strategy_level:
    [ [ IDENT "expand" -> { Conv_oracle.Expand }
      | IDENT "opaque" -> { Conv_oracle.Opaque }
      | n=integer -> { Conv_oracle.Level n }
      | IDENT "transparent" -> { Conv_oracle.transparent } ] ]
  ;

[herbelin]

I added a few other things made by About. Still not exhaustive though. For instance, it also mentions the dependencies in section variables.

[herbelin]

The command description uses "level", seems a better fit than "weight" as well as "expand", which I used in the updated messages.

Then fine to me.

[jfehrle]

Added your changes. Should be ready to merge. Thanks!

[herbelin]

OK, will merge by tomorrow or Wednesday if there are no more comments.

[herbelin]

@coqbot run full ci

[herbelin]

@coqbot run full ci

[jfehrle]

OK, will merge by tomorrow or Wednesday if there are no more comments.

Please?

[herbelin]

@coqbot merge now

[proux01]

Let's not backport a change in output (there is still a little risk that someone relies on it).