The Coq mailing list

[Yevgeniy Makarov <emakarov AT cs.indiana.edu>]

> Hi,
>
> have you read documentation chapter 18 ('Extraction of programs in
> Objective Caml and Haskell', cf.
> <http://pauillac.inria.fr/coq/doc8/Reference-Manual021.html>)?

I cannot use standard Extraction mechanism because, in order to get 
computational content of classical proofs, I cannot ignore 
subderivations of atoms. I'd like to use standard predicates =, <, etc. 
(for example, because then I can use tactics like ring), but then 
derivations of equalities are not included in the extracted program.

Another reason is that there is neither ~ nor double negation 
elimination tactic NNPP for Set.

If I am able to analyze a proof term then I can prove everything with 
respect to Prop and then run functions like or_ind, which are not 
included in the output program if I use Extraction.

Yevgeniy