diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 670d30c6c..66781a8c3 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -303,7 +303,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 " ++ |