diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 3 |
2 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0d4807e163..69d68bd357 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 ff4c18ad21..6ee695bc24 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 " ++ |