From e245e31a6fa3df465f99159999aac6ebbc0b48eb Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 17:12:48 +0100
Subject: [dune] Install coq libraries in `%{lib_root}/coq` instead of `lib`

This is what the native Dune Coq version already does, but it is a
problem for Coq Dune too as noted by @vgbl.
---
 tools/coq_dune.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 41057a79e0..06ad9e4792 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -193,8 +193,8 @@ let pp_dep dir fmt oo = match oo with
 let out_install fmt dir ff =
   let itarget = String.concat "/" dir in
   let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in
-  let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (bpath [itarget;tg]) in
-  fprintf fmt "(install@\n @[(section lib)@\n(package coq)@\n(files @[%a@])@])@\n"
+  let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in
+  fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n"
     (pp_list pp_ispec sep) ff
 
 (* For each directory, we must record two things, the build rules and
-- 
cgit v1.2.3