diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:07 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:07 +0100 |
| commit | 3690e568a36f8b418ec9c253a3188403f53021ba (patch) | |
| tree | 78e428676766abab6fc49dec53c95c3fc89a5d22 /plugins | |
| parent | fcdddca6124eec4d34e1f57a39aadbd2b082ffcf (diff) | |
| parent | 1ed79649c0435336c98a1d8b89e1ccc36b8107cc (diff) | |
Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language command
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 23452febd..24c70bccf 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -42,14 +42,20 @@ 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" +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 ] +| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] +| [ "OCaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] | [ "JSON" ] -> [ JSON ] |