From cf0e030f3aebecb316852fc4a152fb212f9e7ef5 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 5 May 2017 15:58:52 +0200
Subject: coqtop -help: don't die if coqlib can't be found

---
 toplevel/coqtop.ml | 10 +++++++++-
 toplevel/usage.ml  |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5687418f2d..8f50bfb3d8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -292,9 +292,17 @@ let init_gc () =
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
 
+let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
+    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
+
+exception NoCoqLib
 let usage () =
-  Envars.set_coqlib ~fail:CErrors.error;
+  begin
+  try
+  Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
   init_load_path ();
+  with NoCoqLib -> usage_no_coqlib ()
+  end;
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e457ca61d0..e290480354 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -30,6 +30,7 @@ let print_usage_channel co command =
 \n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
 \n  -noinit                start without loading the Init library\
-- 
cgit v1.2.3