Symbol not found is sometimes misleading

[shym]

The message Symbol not found is used in many cases, some of which I find rather hostile to newcomers.

On the following example:

(*@ val g: int -> int *)

val f : int -> int
(*@ r = f x
    ensures r = g x *)

gospel check reports:

File "abc.mli", line 5, characters 16-17:
5 |     ensures r = g x *)
                    ^
Error: Symbol g not found.

This is due to the fact that g was not declared as pure.

The same message is used for r in the following:

val f : int -> int
(*@ r = f x
    requires r = 0 *)

where the result is bound in a requires.

Maybe specific messages should be used in those cases to help users understand what is in scope.

[shym]

#323 proposes to add a documentation page explaining what is in scope in which clauses.
I would propose to reformulate the symbol-not-found error message so that it refers users to that part of the documentation.