doc: fixing some 1-page long overful boxes + common macros.
[smt]: allow specifying the timeout only.

The syntax is `smt maxprovers timeout` where maxprovers/timeout can be
let unspecified (i.e. set to the default value) using `_`.

[fix #17124]
[doc]: relayout all examples s.t. they fit in a page smaller than A0.
test-suite: can give base timeout + timeout factor on a per-file basis.

FSet.ec is now having a factor of 2.
Clear patterns should allow module/memory idents (in parser).

[fix #17125]
Add CLI option + vernacular command to scale timeout for a factor.

CLI option is `-cpu-factor n`. Vernacular command is `timeout *n`.

The option/command scales timeout by `n`.

[close #17126]
In CI: timeout scale now uses the -cpu-factor CLI option.
`make install`: now install all available theories under theories/
Move new theories under theories/newth
Nits on doc/

Remove staled tactic files, fix some notations, document [change].
Add a --weak-check option to the CI script

When set, EasyCrypt is started in weak-check mode.

[close #16780]
foo
Fix bug in `lvalues` typing

When typing a map update, check that the update function returns a type
compatible with the one of the map.

[fix #17127]
[fix #17128]
[fix #17129]
Refactoring: factor out record typing / scheme generation.

[ref #17094]
[fix #17130]
Generic theory axiomatazing subtypes.

This module define the subtype [sT] of [T] defined as {x : T | P x}
where P is a predicate over T. This subtype is defined via an
axiomatization of an inversible partial projection from [T] to [sT]
that respects [P].

Injection from [sT] to [T] and (partial) projection of [T] to [sT]
   val   == generic injection from [sT] to [T]
   insub == generic partial projection from [T] to [sT]

   {x : T | P x} and [sT] are in bijection via val/insub.
      1. insub x = None                  if !(P x)
      2. insub x = Some y with val y = x if  (P x)
Refactoring: factor out datatypes typing / scheme generation.

[ref #17094]
Recast low-error in user-error when `case` fails in an intro-pattern.

[fix #17135]