Revise Identifier implementation

[n-osborne]

If we decide to move forward with #377, unicity of Identifier is expected to be broken across modules. Indeed, the tag in Identifier.Ident.create and Identifier.Ident.of_preid will be reset at every run of the type-checker.

The change should obvioulsy need to preserve equality and comparison in addition to guarantee unicity of identifiers. But I don't think we should be too much concerned about preserving the interface as it is now. For example, I believe one elegant solution would be to resolve identifier with absolute path (I believe it is how it is done in the OCaml compiler). That would implies the two functions above to take a path as extra argument.

[n-osborne]

Apparently, Identifier.t containing only the name and not the path is a problem for translation to Why3 and Coq.

[n-osborne]

Closing as it is superseded and specialised by #411
Also, #389 add fully resolved path