coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] No more info tactical?!

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] No more info tactical?!
Date: Fri, 06 Jan 2012 09:12:16 -0500

Pierre Courtieu wrote:

For this use there is a debug mechanism for Ltac. It has been there
for a while but is now shortly documented
(http://coq.inria.fr/coq/refman/Reference-Manual012.html#@default763).

Set Ltac Debug.

Is this different from [Debug On]?

[Coq-Club] No more info tactical?!, Luke Maurer
- Re: [Coq-Club] No more info tactical?!, Arnaud Spiwack
  - Re: [Coq-Club] No more info tactical?!, Adam Chlipala
    - Re: [Coq-Club] No more info tactical?!, Pierre Courtieu
      - Re: [Coq-Club] No more info tactical?!, Adam Chlipala
        
        Re: [Coq-Club] No more info tactical?!, Pierre Courtieu
        
        Re: [Coq-Club] No more info tactical?!, Adam Chlipala
        
        Re: [Coq-Club] No more info tactical?!, Luke Maurer
        
        Re: [Coq-Club] No more info tactical?!, Paul Broome
        
        Re: [Coq-Club] No more info tactical?!, Arnaud Spiwack
  - Re: [Coq-Club] No more info tactical?!, Luke Maurer
  - Re: [Coq-Club] No more info tactical?!, Jonas B. Jensen