coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Speeding up inversion on large inductives
Date: Wed, 9 Sep 2015 14:28:23 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-la0-f48.google.com
Ironport-phdr: 9a23:MF/KbBE+xvcwmlCb9TnAU51GYnF86YWxBRYc798ds5kLTJ75oMuwAkXT6L1XgUPTWs2DsrQf27aQ6vyrBTxIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6brp9aPM01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4/SXEGCCI/zM3Vngc2k5DBBGA5xXnVL/wtDH7v6xzwn/JE9fxSOUMWDm49aojYxj1kjsGOiNxpHnWh9ZqgeRQpw+7ux1y3qbbZYiUMLx1eaaLLoBSfnZIQssED38JOYi7dYZaSrNZZes=

Hi, you can control the depth of printing with Set Printing Depth
<depth>. (50 by default).

You may want to also control the width of printing then, see:

https://coq.inria.fr/distrib/current/refman/Reference-Manual008.html#sec296

P.

2015-09-09 14:12 GMT+02:00 Petar Maksimovic
<petar.maksimovic AT gmail.com>:
> Javascript

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