coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Andrew McCreight" <continuation AT gmail.com>
- To: Coq-Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] debugging autorewrite?
- Date: Wed, 23 Jul 2008 11:43:26 -0700
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=ofUwGfkj+KoFjEbbYEyG8x+Ywhl8WdVd+5NDlY91JL7LXAVLlPflwU++pJWmESxdW1 4ZL/bIyeKFPYXVjYKCJst898ZuomonLdNleLeOfor9pDSvSUd3giXAQqDCz1AE2ORwul 9D46fPahppjx95BrdroAtPPevu10Q94WJ/T64=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
I'm porting some Coq code from 8.1 to 8.2beta3, and I've hit an instance where using autorewrite appears to go into an infinite loop with 8.2beta3 where it was fine with 8.1. Is there any way to figure out what rules it is applying, or what rule it is applying first? Using 'info' just seems to result in the same infinite loop. Or is there any other way to try to figure out what is going on without just manually applying each rule in the database? Thanks!
-Andrew
I'm porting some Coq code from 8.1 to 8.2beta3, and I've hit an instance where using autorewrite appears to go into an infinite loop with 8.2beta3 where it was fine with 8.1. Is there any way to figure out what rules it is applying, or what rule it is applying first? Using 'info' just seems to result in the same infinite loop. Or is there any other way to try to figure out what is going on without just manually applying each rule in the database? Thanks!
-Andrew
- [Coq-Club] debugging autorewrite?, Andrew McCreight
Archive powered by MhonArc 2.6.16.