coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to control abbreviation of goals / hypothesis in CoIDE?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to control abbreviation of goals / hypothesis in CoIDE?
Date: Tue, 25 Jun 2019 02:06:43 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f47.google.com
Ironport-phdr: 9a23:bsQ61RZBqxDMa59u8bmW6+7/LSx+4OfEezUN459isYplN5qZoMS/bnLW6fgltlLVR4KTs6sC17OM9fm8EjRRqdbZ6TZeKcUKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZ8Jqor1xfErXREd/hSyGh1IV6fgwvw6t2/8ZJ+7ihcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd4QAD+QDMuhYoYfzpEYAowWiCgS3Huzj1iVFi2Xq0aEm0eksFxzN0gw6H9IJtXTZtNH7O70JUeCyyqnD0DTNb+lR2Tfm84jDbxcsofOWUrJrdsrRz0YvFxnCjlWLsozoOyiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhIfOhoIQ0F/E9CN5zZ40Jd2+VE50f9qkHIFNuC6EMYZ9X8AsQ3lwtSok1rELvYS3cSsKxZg92RLTd/+Kf5KH7x/hUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtKqzBKktjItnwUyRPc99WLRuJz/kqu2zuDzQ/T6uZDIUA7karUNYQtzaI3lpoWqUjDHyn2l1vqjKKOaEko5uyl5/7kb7jmvJOQKZN4hwLkPqkhmMGzGeE4PRIPX2if9+S8zrrj/UjhTbVIlPI2ia7ZsJbVJcQBoa65GBRV34I45hawCjepytUYnX0dIF1ZfxKHipDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDUyrbCaiAdajWrFWg5+Q1IuDKapVD6xjnLP1wxff1inlxtkUaZrLhiZkec3e+Ee5hOF7ISXXpi9YFV2wNu1xtH6TRlFSeXGsLND6JVKUm62RjUdP0PcL4XomoxYe58mK+F5xSaHpBDwnVQ3jtfoSAHfwLbXDLe5Izonk/TbGkDrQZ+1SuuQv9kec1K+PV/mgVucum2oQqoeLUkh42+Hp/CMHPizjRHVExpXsBQnoN5I46uVZ0kw7R3q1xgvgeHttWtatE

I believe the option you're looking for is Set Printing Depth 1000000 (or some similarly large number... unfortunately, there is no Set Printing Depth Unlimited option)

On Tue, Jun 25, 2019, 01:44 Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Team,

lengthy goals and hypothesis are abbreviated by CoqIDE (or more likely coqtop – not sure) with ellipses. I can’t find an option to expand this or to control the limits for this. I am working on VST verification of some optimized numerical C function which happens to have quite a few local variables which leads to lengthy, but not complicated, separation logic contexts.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] How to control abbreviation of goals / hypothesis in CoIDE?, Soegtrop, Michael, 06/25/2019
- Re: [Coq-Club] How to control abbreviation of goals / hypothesis in CoIDE?, Jason Gross, 06/25/2019