| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
For instance:
Extract Inductive nat => int [ "0" "succ" ]
"(fun fO fS n => if n=0 then fO () else fS (n-1))".
See Extraction.v for more details and caveat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|