summaryrefslogtreecommitdiff
path: root/plugins/extraction/g_extraction.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
-rw-r--r--plugins/extraction/g_extraction.ml42
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3caa558f..3fe5a8c0 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -41,12 +41,14 @@ let pr_language = function
| Ocaml -> str "Ocaml"
| Haskell -> str "Haskell"
| Scheme -> str "Scheme"
+ | JSON -> str "JSON"
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
| [ "Ocaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
+| [ "JSON" ] -> [ JSON ]
END
(* Extraction commands *)