From 1c34e2244e77a0759bf7a5b6925643de8fe133b5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 11 Jun 2019 03:49:31 +0200
Subject: [dune] Move to Dune 1.10, use coq.pp directive.

We use the `(coq.pp ...)` dune directive which will produce correct
error messages for `.mlg` files.

Unfortunately we cannot yet use the automatic opam generation features
of Dune 1.10, as this does require a fully native Dune build.

Dune 1.6-1.10 has quite a few other improvements that could be used by
Coq, for example for promote modes.

I have fixed a couple of documentation issues. `Drop` and `ocamldebug`
have been tested in this version.
---
 tools/coq_dune.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 1920d493de..adb416e3ce 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -193,9 +193,7 @@ let pp_vo_dep dir fmt vo =
   pp_rule fmt all_targets deps action
 
 let pp_mlg_dep _dir fmt ml =
-  let target = Filename.(remove_extension ml) ^ ".ml" in
-  let mlg_rule = "(run coqpp %{pp-file})" in
-  pp_rule fmt [target] [ml] mlg_rule
+  fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml)
 
 let pp_dep dir fmt oo = match oo with
   | VO vo -> pp_vo_dep dir fmt vo
-- 
cgit v1.2.3