diff options
| author | Guillaume Melquiond | 2015-04-02 14:24:48 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-02 14:30:00 +0200 |
| commit | 933744fefc85da267ef8304e89e6e414bb960cce (patch) | |
| tree | 62ff426145ccf3b9672d9fcddea5ada4ee4d533d /plugins/syntax/string_syntax_plugin.mllib | |
| parent | afaeab91f8206986dbbb7f245d61e4a0d185050c (diff) | |
Remove Mltop.add_path as it is no longer possible to import files from subdirectories.
Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:
$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.
The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.
This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mllib')
0 files changed, 0 insertions, 0 deletions