[ re #5267 ] Add new infective options to user manual

doc/user-manual/tools/command-line-options.rst

@@ -1699,15 +1699,20 @@ An *infective* option is an option that if used in one module, must be
 used in all modules that depend on this module. The following options
 are infective:
 
+* :option:`--allow-exec`
 * :option:`--cohesion`
 * :option:`--cumulativity`
 * :option:`--erased-matches`
 * :option:`--erasure`
+* :option:`--experimental-irrelevance`
 * :option:`--flat-split`
 * :option:`--guarded`
+* :option:`--injective-type-constructors`
+* :option:`--omega-in-omega`
 * :option:`--prop`
 * :option:`--rewriting`
 * :option:`--two-level`
+* :option:`--type-in-type`
 
 Furthermore :option:`--cubical` and :option:`--erased-cubical` are
 *jointly infective*: if one of them is used in one module, then one or