coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Conversion raised an anomaly"

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] "Conversion raised an anomaly"
Date: Wed, 6 Jul 2016 13:22:36 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:j9zKghYTwamTdXfzR6ISWar/LSx+4OfEezUN459isYplN5qZpcmzbnLW6fgltlLVR4KTs6sC0LuO9fq+EjZZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxjb75ocSbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jAsgCLZg+S7DNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPF8DqRPgGWDCj5qFqAEvihTsOHzsh8STMldc2i7hU9kHy7ydjypLZNdnGfMF1ebnQKJZDHTJM

This is primarly targeted to the devs in the list.

I have a tactic that produces a term that, apparently, makes some Reductionops function fail with the error message "Conversion raised an anomaly". Oddly enough, if I copy the (Set Printing All) term, and pose it, it works, so the term is well constructed (modulo universes). Does anyone have an idea what can be happening, or how can I get further information on the issue?

Thanks,

Beta

[Coq-Club] "Conversion raised an anomaly", Beta Ziliani, 07/06/2016
- Re: [Coq-Club] "Conversion raised an anomaly", Matthieu Sozeau, 07/06/2016
  - Re: [Coq-Club] "Conversion raised an anomaly", Beta Ziliani, 07/07/2016