The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi coq-club,

Currently, coqwc counts ‘Ltac :=’ tactics as specifications. Can this be 
changed? Alternatively, are there other tools to summarize the contents of a 
Coq development?

As an example, coqwc thinks that this snippet has 12 lines of specifications, 
and a single line of proofs:

    Ltac cleanup :=
      match goal with
      | _ => tauto
      | _ => discriminate
      | _ => progress intros
      | _ => progress subst
      | [ |- ?a <-> ?b ] => split
      | [  |- ?a /\ ?b ] => split
      | [ H: ?a /\ ?b |- _ ] => destruct H
      | [ H: exists _, _ |- _ ] => destruct H
      end.

    Goal True.
      cleanup.
    Qed.

whereas it summarizes the following snippet as 1 line of specs and 11 lines 
of proofs:

    Goal True.
      match goal with
      | _ => tauto
      | _ => discriminate
      | _ => progress intros
      | _ => progress subst
      | [ |- ?a <-> ?b ] => split
      | [  |- ?a /\ ?b ] => split
      | [ H: ?a /\ ?b |- _ ] => destruct H
      | [ H: exists _, _ |- _ ] => destruct H
      end.
    Qed.

Is there a way to make coqwc return the same numbers (approx. 1 line of 
specs, 10 lines of proofs) for both snippets? Patching and recompiling is 
totally fine, if needed.

Thanks!
Clément.

Attachment: signature.asc
Description: OpenPGP digital signature