Pierre Villemot

I think we should forbid such redefinitions but we can do it after the next release.

The PR is ready for a second pass. I think we should test the legacy frontend with `fpa` on Marvin before merging it.

I rebase this PR on #1117 to remove some polymorphic comparisons again ;)

No regression with the following combinations: - frontend `legacy` on `ae-format` - frontend `legacy` on `ae-format-fpa` with `--enable-theories fpa` - frontend `dolmen` on `ae-format` - frontend `dolmen` on `ae-format-fpa` with...

After consideration, adding definitions to the input problem won't solve the issue because this definition will probably involve quantifiers and Dolmen doesn't support model checking of quantified problems.

I also found a wrong message from the type checker with this input file: ``` (set-logic ALL) (declare-const x Int) (declare-const y Bool) (declare-fun f (Int Int) Int) (assert (=...

It seems that the action `ocaml-setup`does not yet support MSYS2. Currently, the action runs opam with Cygwin, which is not what we want. I opened an issue https://github.com/ocaml/setup-ocaml/issues/846.

Good news, Alt-Ergo works on Windows through Opam 2.2 now! We support installations with both MSYS2 and Cygwin. You can try to setup it with: ``` opam pin https://github.com/OCamlPro/alt-ergo.git#next ```...

> Sorry for this long silence, I was in vacation ^^. > > I installed the package this morning and got the following warning: > > ``` > [WARNING] C:\Users\ab238114\AppData\Local\opam\default\bin\alt-ergo.exe...

I tried again yesterday with a fresh installation of opam and I couldn't reproduce the bug. Could you try to run Alt-Ergo in bash with a dummy input? We may...