aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 21:45:47 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 21:45:47 +0000
commit1c450e282d8e6ae37f687c545776939f2d975cf3 (patch)
treefd0f3796a07516776016234f162374942db0b1d9 /doc
parentbfc03c53882d7334e4fb327362c354397a8462ba (diff)
Correct enormous bug in interpretation of generalized binders: it simply
dropped all bindings appearing before it :) Bug found by Marc Lasson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions