diff options
| author | Guillaume Melquiond | 2015-04-02 13:36:43 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-02 14:14:16 +0200 |
| commit | 049f329908ab6702c3a933ddc45ae6b6f5160065 (patch) | |
| tree | 97078cea381a324edd771913139ea565164e26b6 /kernel/type_errors.mli | |
| parent | 27a87e4487c8b926aa0ed6c0ab65333d4ef5c3bc (diff) | |
Make it possible for -R to override the existing implicit setting of a path.
Without this commit, passing "-R theories Coq" to "coqtop -nois" has no
effect since "-Q theories Coq" has already been done implicitly.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions