From 50771329244484b220a9eab0d7e9fe9f15c194a3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 12 Apr 2019 15:27:16 +0200
Subject: [PATCH] [coq] Rename `(coqlib ...)` to `(coq.theory ...)`

Support for the first form will be dropped in the 1.0 version of the
Coq language.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
---
 CHANGES.md                                            |  4 ++++
 doc/coq.rst                                           |  6 +++---
 src/dune_file.ml                                      | 11 +++++++++--
 test/blackbox-tests/test-cases/coq/base/dune          |  2 +-
 .../test-cases/coq/ml_lib/theories/dune               |  2 +-
 test/blackbox-tests/test-cases/coq/rec_module/dune    |  2 +-
 6 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 1835da3d001..a31001bd672 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,10 @@
 unreleased
 ----------
 
+- [coq] Rename `(coqlib ...)` to `(coq.theory ...)`, support for
+  `coqlib` will be dropped in the 1.0 version of the Coq language
+  (#2055, @ejgallego)
+
 - [coq] Add `coq.pp` stanza to help with pre-processing of grammar
   files (#2054, @ejgallego, review by @rgrinberg)
 
diff --git a/doc/coq.rst b/doc/coq.rst
index 6f9c8834004..7039a35d006 100644
--- a/doc/coq.rst
+++ b/doc/coq.rst
@@ -14,9 +14,9 @@ in the ``dune-project`` file. For example:
 
     (using coq 0.1)
 
-This will enable support for the ``coqlib`` stanza in the current project. If the
+This will enable support for the ``coq.theory`` stanza in the current project. If the
 language version is absent, dune will automatically add this line with the
-latest Coq version to the project file once a ``(coqlib ...)`` stanza is used anywhere.
+latest Coq version to the project file once a ``(coq.theory ...)`` stanza is used anywhere.
 
 
 Basic Usage
@@ -26,7 +26,7 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
 
 .. code:: scheme
 
-    (coqlib
+    (coq.theory
      (name <module_prefix>)
      (public_name <package.lib_name>)
      (synopsis <text>)
diff --git a/src/dune_file.ml b/src/dune_file.ml
index 66407de90d5..8483356a00c 100644
--- a/src/dune_file.ml
+++ b/src/dune_file.ml
@@ -1886,11 +1886,18 @@ module Coq = struct
 
   let unit_to_sexp () = Sexp.List []
 
-  let coqlib_p = "coqlib", decode >>| fun x -> [T x]
+  let coqlib_warn x =
+    Errors.warn x.loc
+      "(coqlib ...) is deprecated and will be removed in the Coq \
+       language version 1.0, please use (coq.theory ...) instead";
+    x
+
+  let coqlib_p = "coqlib", decode >>| fun x -> [T (coqlib_warn x)]
+  let coqtheory_p = "coq.theory", decode >>| fun x -> [T x]
   let coqpp_p = "coq.pp", Coqpp.(decode >>| fun x -> [T x])
 
   let unit_stanzas =
-    let+ r = return [coqlib_p; coqpp_p] in
+    let+ r = return [coqlib_p; coqtheory_p; coqpp_p] in
     ((), r)
 
   let key =
diff --git a/test/blackbox-tests/test-cases/coq/base/dune b/test/blackbox-tests/test-cases/coq/base/dune
index e19b3f2716c..ea7e7214d52 100644
--- a/test/blackbox-tests/test-cases/coq/base/dune
+++ b/test/blackbox-tests/test-cases/coq/base/dune
@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name basic)
  (public_name base.basic)
  (modules :standard)
diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune b/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune
index 724342cef44..736a5e9f4a3 100644
--- a/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune
+++ b/test/blackbox-tests/test-cases/coq/ml_lib/theories/dune
@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name Plugin)
  (public_name ml_lib.Plugin)
  (synopsis "Test Plugin")
diff --git a/test/blackbox-tests/test-cases/coq/rec_module/dune b/test/blackbox-tests/test-cases/coq/rec_module/dune
index cb281e99db4..b447b3e1da9 100644
--- a/test/blackbox-tests/test-cases/coq/rec_module/dune
+++ b/test/blackbox-tests/test-cases/coq/rec_module/dune
@@ -1,4 +1,4 @@
-(coqlib
+(coq.theory
  (name rec_module)
  (public_name rec.module)
  (modules :standard)