coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Speeding up inversion on large inductives

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Speeding up inversion on large inductives
Date: Wed, 9 Sep 2015 08:38:33 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:78uDZB3FfdIYrZm0smDT+DRfVm0co7zxezQtwd8ZsegSL/ad9pjvdHbS+e9qxAeQG96Lt7Qd16GK4+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZ3rnLzis7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCCLZ34RVHkhqhtURk3u6BjnUpr1+n/xsud41S+Ge9X3UZg7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

On 09/09/2015 08:12 AM, Petar Maksimovic wrote:
> On a side note, is there a way, when doing Check ________, of
> instructing Coq to print the statement fully, without putting two dots
> (..) in places where it estimates the printout would be too large or
> poorly formatted?

[Set Printing Depth (some large number).] should do
(https://coq.inria.fr/refman/Reference-Manual008.html#sec302)
See also [Redirect],
https://lists.gforge.inria.fr/pipermail/coq-commits/2015-May/014808.html

Clément.

Re: [Coq-Club] Speeding up inversion on large inductives, (continued)
- Re: [Coq-Club] Speeding up inversion on large inductives, Gregory Malecha, 09/08/2015
  - Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/09/2015
    - Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/09/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Pierre Courtieu, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Clément Pit--Claudel, 09/09/2015