ocaml-maint team mailing list archive

[Gianfranco Costamagna <costamagnagianfranco@xxxxxxxx>]

this is fixed since a long time...

** Changed in: alt-ergo (Ubuntu)
       Status: New => Incomplete

** Changed in: alt-ergo (Ubuntu)
       Status: Incomplete => Fix Released

-- 
You received this bug notification because you are a member of Debian
OCaml Maintainers, which is subscribed to alt-ergo in Ubuntu.
https://bugs.launchpad.net/bugs/1134259

Title:
  Alpha-conversion bug in alt-ergo 0.94

Status in alt-ergo package in Ubuntu:
  Fix Released

Bug description:
  There is a rather serious alpha-conversion bug in alt-ergo 0.94
  (available in Ubuntu 12.10). Try this:

  goal absurd: (forall b:bool. b = true) or (forall b:bool. b = false)

  Observed behavior: alt-ergo says this is valid.
  Expected behavior: alt-ergo should not be able to prove this.

  Note that this is fixed in alt-ergo 0.95, however this version is not
  available in the Ubuntu repos.

  Best,

  Malte

To manage notifications about this bug go to:
https://bugs.launchpad.net/ubuntu/+source/alt-ergo/+bug/1134259/+subscriptions