Guillaume Bury
Guillaume Bury
Great news ! Thanks a lot for your work !
There has been some discussions about order of definitions in models, and it is still ongoing (see https://github.com/SMT-LIB/SMT-LIB-2/issues/26). For what it's worth, even though keeping the same order as the...
I tried using the new anchors, but on my machine (a linux one), if I try to go explicitly to the windows instructions from a link (i.e. https://ocaml.org/install#windows or even...
I'd say the ideal scenario would be to have all the following points be true: - when someone follows a link to `https://ocaml.org/install`, redirect to the page that matches the...
oops, let me fix that
Actually, now that `ocaml.org` produces and hosts packages's documentation (e.g, see https://ocaml.org/p/dolmen/latest/doc/index.html for the doc of the main dolmen package), maybe the link should simply redirect to that page ?
Any idea why the tests in `tests/cram.t/run.t` do not catch the error ? these tests should exercise the case where there is a prelude, and there is an error in...
Thanks ! As discussed offline, any primitive that is officially part of the alt-ergo's native language (something that you can actually decide as an alt-ergo dev), should indeed be implemented...
That makes sense to me. i'm in favor of removing Tableaux-CDCL, and investigating the cases where CDCL is better so that we can consider removing it in the future.
@bobot I opened a PR in your repository against this branch since I couldn't push to it directly: https://github.com/bobot/opam-repository/pull/1