aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorjforest2008-11-23 20:31:14 +0000
committerjforest2008-11-23 20:31:14 +0000
commit31eac37de7a01bf67be3e5547792794f97142f25 (patch)
tree72b1aa46db7737251b059edb2a342d7ab52abfb8 /dev
parent1e77a259834aa570a0ff41be7b9ba3f9e81cfe52 (diff)
first attempt to allow Function to deal with dependent pattern matching. This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions