diff options
| author | Hugo Herbelin | 2019-05-11 22:20:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-08 11:52:00 +0200 |
| commit | cb60825aec0f6ff79b7a7a3f21c1ab4d8e11dae7 (patch) | |
| tree | 9e644c17b1a263c9221edf50f7aa57ada0544c69 /kernel/nativelib.ml | |
| parent | 0d97f184408ffd50d11608f0e73ac3edaf1193ca (diff) | |
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.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions