The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Indeed the -o option here is not precise enough.

would it make sense to submitting a feature wish for some [coqchk
-print-assumptions-for foo] option?

P.






2015-03-30 11:04 GMT+02:00 Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>:
> If you have a better behaviour to suggest for `coqchk` please do. But I'm
> not sure it will be easy, unfortunately.
>
> On 29 March 2015 at 19:54, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>>
>>
>>
>> On 03/29/2015 01:41 PM, Enrico Tassi wrote:
>>>
>>> On Sun, Mar 29, 2015 at 01:27:25PM -0400, Jonathan Leivent wrote:
>>>>
>>>> Even worse - a file that just says:
>>>>
>>>>   Require Import EquivDec.
>>>>
>>>> when run through coqchk -o will produce:
>>>
>>> Coqchk prints all the axioms, as in "Axiom" keyword, loaded in the
>>> environment.  "Print Assumptions name" prints only the ones used by
>>> name.
>>>
>>> Best,
>>
>>
>> Right - I should have inferred that.  Although that coqchk -o behavior
>> seems not too useful, in that case.
>>
>> -- Jonathan
>>
>>
>