coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: t x <txrev319 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Dumping everything from a list of Modules
- Date: Fri, 19 Jul 2013 08:43:33 -0700
Hi,
I want to dump Lemmas + Inductive definitions + Records from a list of modules in a machine parseable way.
I currently have the following:
>> echo "Require Import List ZArith. Unset Printing Notations. SearchAbout(_)." | coqtop.opt > lst
What I'm currently lacking are (1) inductive definitions and (2) records. What is the easiest way to access this information?
Thanks!
- [Coq-Club] Dumping everything from a list of Modules, t x, 07/19/2013
Archive powered by MHonArc 2.6.18.