Remove Coq-Equations plugin dependency

[dgarbuzov]

Requiring the Coq-Equations plugin substantially complicates the build process by introducing a dependency on the version of OCaml and camlp4. It is also only used in a single file, the patched Values.v from compcert, and it's unclear why it's really necessary. It shouldn't be too difficult to remove.

[jeehoonkang]

I agree with you in removing dependency to Coq-Equations, but in a slightly different reason. I would like to use ssreflect library developed by George Gonthier. However, ssreflect can be compiled only if Coq is compiled with camlp5. Thus I would like to remove dependency to camlp4, that also means removing dependency to Coq-Equations.

[catalin-hritcu]

Has there been any progress on removing this dependency? Wanted to have a quick look, but I've already wasted hours making the original SoftBound to compile ... out of time to kill for now.

[Zdancewic]

Sorry, we haven't found the time to do that yet!