Typos.
micromega : refification recognises @eq T for T convertible with Z or R
Removing the call to Weak.get_copy in hashsets.

The rationale for its use comes from OCaml weak maps, and is justified by the
fact that Weak.get may prevent its return value to be collected by the GC during
the next slice even though nobody points to it. In our case, this is vastly
irrelevant because hashconsed values are not expected to be collected whatsoever
(save for exceptional cases). But Weak.get_copy is rather costly actually, at
least strictly more than the plain Weak.get.

Experimentally, I observe diminution of compilation time and even diminution
of memory consumption (!) after this patch, so I assume it is a net gain.
Making the error message about bullets more precise.
Suggests in some cases the right bullet to use.
Useless export of Instance.eqeq. We hashcons everything before calling this
function, so plain pointer equality is sufficient.