coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] How to control abbreviation of goals / hypothesis in CoIDE?
Date: Tue, 25 Jun 2019 08:44:01 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:grB+gxy2xiIeP/DXCy+O+j09IxM/srCxBDY+r6Qd2+IRIJqq85mqBkHD//Il1AaPAdyBrasYwLKL++C4ACpcuM/H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjPusUMnIdvJak9xgfJr3BVf+ha2X5kKUickhrh+8u85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnHUwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhSwaKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyxPDJ2hYYsTAeQPPudYoJXyqFYVtxSyGRWgCfnzxjNUmHP727Ax3eQ7EQHB2QwtB9wCvmnTrNrrO6cSTfq1zK7QzTnbcvhY3jb955TIch87v/6MWbx8etfWxEkqFgPKklWQppb7MDORzOgNqG+b4PRvVeKzkW4nrBlxryOuxscqlonGmIYVxkrY+iV+xYY4PNu1Q1N1b96jFZtfrSCaN41uT8MjRWFopDg1yrkctZGmYicHzoksyR3Ha/GfboSF5gzvWPyRLDp4nn5oeKyziwyv/US+1uHwTtS43VdEoyZfnNTBuGoB2wLd58WDUPdx40Ss1SqX2wzO6+xJJVo4mbTbJpMu2LI8iIAfvVnDEyLynkj9kbWYeV8++uey7uTqerXmqYGYN49zkgz+N6suldajDek3KAQOXm6b+fii273n50H2XLJKjvgunqnYtpDVO9gbq7akDwJRzIov8RayAje83NkYg3ULNk9JdAybg4TxPlHBOvH4DfOxg1S2lzdrwujLPrjgAprRLnjMiqnufbJn505Hzwo8099f545OCrEGOPL+QU7xtNrEDhAnNwy42froCNJ41o8GQ2KAHreZML/OsV+P/u8gP+6MZJYMtDnhL/gl+uXhgGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7mgg1qbFDVXenyaXqQm5zh9BpjsRdPIQZnoi7ic1g+6GIdXbyZIEAbfP23vctDOYPABZz6IJdcl2hkFXrioRotrnUWrtQT6wrdjaPHT9yIEr5X7/Nlz++DX0xo18GonXIymz2iRQjQszSszTDgs0fUn+B0v+hK4yaF9xsdgO5lW7vJNXB09MMeFne18F932HAnGe4XQEQr0cpCdGTg0C+kJ7ZoWeU8kQoejiAzO22yhBLpHz+XWVqxxybrV2j3KH+g4y3vC0/B+3VwpS5MTc2ygmqN7sQPUAtyRng==

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