The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Suppose I define a bst_insert function as in the attached file, and
then in the extraction I want to drop the l and r parameters in the
binary_search_tree type and the bst_insert function.  First of all,
this doesn't work the way I'd expect:

Extraction Implicit empty_bst [l r].
Extraction Implicit bst_node [l r].

It looks like it's making nothing implicit in empty_bst, and the wrong
arguments implicit in bst_node.  (Looks like a probable bug.)  I can
fix that by instead saying:

Extraction Implicit empty_bst [1 2].
Extraction Implicit bst_node [1 2].

Then the extraction of the binary_search_tree type looks like what I'd
expect.  But I haven't been able to find any Extraction Implicit
declarations which will allow bst_insert to extract, using either
parameter names or parameter numbers.

Also, on a minor note, would there be any way to get rid of the type
dependency in comparison_pf, which doesn't make sense in the extracted
version?

(All this is using 8.3pl4.)
-- 
Daniel Schepler

Attachment: BST.v
Description: Binary data