aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
authorherbelin2011-11-16 08:46:56 +0000
committerherbelin2011-11-16 08:46:56 +0000
commite81c1643642459225f895e9328b407329de82071 (patch)
tree7ad4a38536cfb90aa732b714db9bf0a9c4122b39 /plugins/syntax
parentd305fd7ce51e71ddc49901cb86b7394ea51705d3 (diff)
De Bruijn indices bug in pattern matching compilation in the presence
of dependent types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14667 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions