diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/parse.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index eb574a4385..6a99aedc8c 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -443,8 +443,6 @@ Libobject.relax true; begin add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]); - add_path (Filename.concat coqdir "tactics") - (Names.make_dirpath [Nameops.coq_root]); add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]) end; |