Extraction: an experimental command to get rid of some cst/constructor arguments

 The command : Extraction Implicit foo [1 3].
 will tell the extraction to consider fst and third arg of foo as implicit,
 and remove them, unless a final occur-check after extraction shows they
 are still there. Here, foo can be a inductive constructor or a global
 constant.

 This allow typicaly to extract vectors into usual list :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12982 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions