coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marc.Bezem AT uib.no
- To: coq-club AT inria.fr
- Cc: Stefano Piceghello <Stefano.Piceghello AT uib.no>
- Subject: [Coq-Club] unfold makes goal ill-typed
- Date: Thu, 06 Oct 2016 20:15:01 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Marc.Bezem AT uib.no; spf=None smtp.mailfrom=nmimb AT webmail.uib.no; spf=None smtp.helo=postmaster AT alfons.uib.no
- Ironport-phdr: 9a23:BAX5RxZsUE8YQQhcMESzisr/LSx+4OfEezUN459isYplN5qZpsu8bnLW6fgltlLVR4KTs6sC0LuM9fu6EjVZvt7B6ClEK8McEUddyI0/pE8JPo2sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx+z+7e25+oXSbgNUn3L9JOoqdFTl5TnW48IRmM5pLrs74hrPuHpBPepMlk1yIlfGuh/m7YGa8Yxu9gxNuvhn8ckTAu3BY60kQOkAX3wdOGcv6Ziu7EGbQA==
Has anybody observed that an unfold can make a goal ill-typed?
I'm asking this to find out whether this is a coq bug or a user error.
The situation in which it happens is quite complicated, and the ill-typed goal lived on for quite a while. From the point where the goal became visibly ill-typed I could trace back (all the time testing the goal with Check), and the command that first made the goal ill-typed was a rather harmless unfold. It will be a challenge to isolate the behaviour in a simple example.
All help will be appreciated.
Marc
- [Coq-Club] unfold makes goal ill-typed, Marc . Bezem, 10/06/2016
- Re: [Coq-Club] unfold makes goal ill-typed, Jason Gross, 10/06/2016
Archive powered by MHonArc 2.6.18.