From 6d20e4c136fb2726ec8577bdfee051ecacdf8261 Mon Sep 17 00:00:00 2001
From: Yves Bertot <yves.bertot@inria.fr>
Date: Wed, 28 Sep 2016 16:24:51 +0200
Subject: fix bug 3683 : adds references to the web site for the bug tracker in
 error messages

---
 checker/checker.ml    | 3 ++-
 config/coq_config.mli | 1 +
 configure.ml          | 1 +
 lib/cErrors.ml        | 4 +++-
 toplevel/coqloop.ml   | 4 +++-
 toplevel/himsg.ml     | 3 ++-
 6 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/checker/checker.ml b/checker/checker.ml
index 0c411ae44..503697b59 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -209,7 +209,8 @@ let usage () =
 open Type_errors
 
 let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report.")
+let report () = (str "." ++ spc () ++ str "Please report" ++
+                 strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
 
 let guill s = str "\"" ++ str s ++ str "\""
 
diff --git a/config/coq_config.mli b/config/coq_config.mli
index a0e1019fa..6087c0116 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -62,6 +62,7 @@ val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
 
 val wwwcoq : string
 val wwwrefman : string
+val wwwbugtracker : string
 val wwwstdlib : string
 val localwwwrefman : string
 
diff --git a/configure.ml b/configure.ml
index 2c1d531ea..23ec93e07 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1043,6 +1043,7 @@ let write_configml f =
   pr "let with_geoproof = ref %B\n" !Prefs.geoproof;
   pr_s "browser" browser;
   pr_s "wwwcoq" !Prefs.coqwebsite;
+  pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/");
   pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/");
   pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1459141d1..c69c7e400 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+           str ".")
   else
     hov 0 (raw_anomaly e)
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0d4807e16..69d68bd35 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -348,5 +348,7 @@ let rec loop () =
     | any ->
       Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
                 str (Printexc.to_string any) ++
-                fnl() ++ str"Please report.");
+                fnl() ++
+                str"Please report" ++
+                strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
       loop ()
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ff4c18ad2..6ee695bc2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -304,7 +304,8 @@ let explain_unification_error env sigma p1 p2 = function
         else []
      | MetaOccurInBody evk ->
         [str "instance for " ++ quote (pr_existential_key sigma evk) ++
-	strbrk " refers to a metavariable - please report your example"]
+	strbrk " refers to a metavariable - please report your example" ++
+        strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."]
      | InstanceNotSameType (evk,env,t,u) ->
         let t, u = pr_explicit env sigma t u in
         [str "unable to find a well-typed instantiation for " ++
-- 
cgit v1.2.3