coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] debugging facilities

From: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
To: Kirill Taran <coq-club AT inria.fr>
Subject: Re: [Coq-Club] debugging facilities
Date: Wed, 12 Mar 2014 15:09:44 +0200

Hello.

Please describe what kind of tracing/debugging
you need. Small example would be the best.

As for cbv, it's not mandatory. You can use
other tactics to reduce expressions: simpl,
compute. Also you can reduce expressions
under "breakpoints".

[Coq-Club] debugging facilities, Kirill Taran, 03/12/2014
- Re: [Coq-Club] debugging facilities, Cedric Auger, 03/12/2014
  - Re: [Coq-Club] debugging facilities, Kirill Taran, 03/12/2014
    - Re: [Coq-Club] debugging facilities, Dmitry Grebeniuk, 03/12/2014
      - Re: [Coq-Club] debugging facilities, Kirill Taran, 03/12/2014