coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coverage tool

From: Duckki Oe <duckki AT mit.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] coverage tool
Date: Thu, 20 Jun 2013 15:00:20 -0400

Hi,

Is there a tool that can detect unreferenced definitions/theorems in a module
(or modules)? I'd like to clean up my modules and remove unnecessary lemmas.
But, I put lemmas in hint databases and it'll be very time consuming to
manually test if every single lemma is used. Thanks!

-- Duckki

[Coq-Club] coverage tool, Duckki Oe, 06/20/2013
- Re: [Coq-Club] coverage tool, Kenneth Adam Miller, 06/21/2013
  - Re: [Coq-Club] coverage tool, Math Prover, 06/21/2013
    - Re: [Coq-Club] coverage tool, Jason Gross, 06/21/2013
      - Re: [Coq-Club] coverage tool, Nuno Gaspar, 06/21/2013
        
        Re: [Coq-Club] coverage tool, Jason Gross, 06/21/2013
        
        Re: [Coq-Club] coverage tool, Duckki Oe, 06/23/2013
        
        Re: [Coq-Club] coverage tool, Harley D. Eades III, 06/24/2013
        Re: [Coq-Club] coverage tool, Nuno Gaspar, 06/24/2013
        
        Re: [Coq-Club] coverage tool, Jason Gross, 06/24/2013