Command line: adding variants for Require, aligning on the vernac syntax.

We deprecate -require (= Require Import) to avoid the confusion with Require.

We propose a regular equivalent to all vernac variants in expanded and
short version:
-require-import, -require-export
-require-import-from, -require-export-from
-ri, -re
-rifrom, -refrom

We also add -rfrom, but wait for the end of deprecation of -require to
replace -load-vernac-object by -require and to introduce a shorthand
-r for the new -require.

0 files changed, 0 insertions, 0 deletions