From 2f75c8b43588ec3094539d95b4c2740805f2ee84 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 4 Apr 2021 15:50:18 +0200
Subject: [coqpp] Add -help

Closes #9932
---
 coqpp/coqpp_main.ml | 25 +++++++++++++++++++++----
 1 file changed, 21 insertions(+), 4 deletions(-)

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 2de103a2ff..748f50b54b 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -615,12 +615,29 @@ let pr_ast fmt = function
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
 | ArgumentExt arg -> fprintf fmt "%a@\n" ArgumentExt.print_ast arg
 
-let () =
+let help () =
+  Format.eprintf "Usage: coqpp file.mlg@\n%!";
+  exit 1
+
+let parse () =
   let () =
-    if Array.length Sys.argv <> 2 then fatal "Expected exactly one command line argument"
+    if Array.length Sys.argv <> 2
+    then help ()
   in
-  let file = Sys.argv.(1) in
-  let output = Filename.chop_extension file ^ ".ml" in
+  match Sys.argv.(1) with
+  | "-help" | "--help" -> help ()
+  | file -> file
+
+let output_name file =
+  try
+    Filename.chop_extension file ^ ".ml"
+  with
+  | Invalid_argument _ ->
+    fatal "Input file must have an extension for coqpp [input.ext -> input.ml]"
+
+let () =
+  let file = parse () in
+  let output = output_name file in
   let ast = parse_file file in
   let chan = open_out output in
   let fmt = formatter_of_out_channel chan in
-- 
cgit v1.2.3