From 600c1ee611a0442fd6794248327a72c53c3d4cb6 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 5 Dec 2017 11:21:31 -0500
Subject: use \ocaml macro in Extraction chapter; accept OCaml in Extraction
 Language

---
 plugins/extraction/g_extraction.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 23452febdc..7cebf5d70e 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -42,14 +42,15 @@ ARGUMENT EXTEND int_or_id
 END
 
 let pr_language = function
-  | Ocaml -> str "Ocaml"
+  | Ocaml -> str "OCaml"
   | Haskell -> str "Haskell"
   | Scheme -> str "Scheme"
   | JSON -> str "JSON"
 
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ Ocaml ] (* deprecated *)
+| [ "OCaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
 | [ "JSON" ] -> [ JSON ]
-- 
cgit v1.2.3


From 1ed79649c0435336c98a1d8b89e1ccc36b8107cc Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 6 Dec 2017 11:29:03 -0500
Subject: issue deprecation warning for "Ocaml"

---
 plugins/extraction/g_extraction.ml4 | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 7cebf5d70e..24c70bccfb 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -47,9 +47,14 @@ let pr_language = function
   | Scheme -> str "Scheme"
   | JSON -> str "JSON"
 
+let warn_deprecated_ocaml_spelling =
+  CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+    (fun () ->
+      strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ] (* deprecated *)
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
 | [ "OCaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
-- 
cgit v1.2.3