coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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

It is the same command.
P.

2012/1/6 Adam Chlipala
<adamc AT csail.mit.edu>:
> 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