aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
diff options
context:
space:
mode:
authorherbelin2010-03-28 19:35:03 +0000
committerherbelin2010-03-28 19:35:03 +0000
commit1c4a4908a82e2eba9cc2d335697d51182f7314c2 (patch)
tree39f6a5b7caf7d583af468d59c9f62378a748f8d3 /dev/tools
parentbe76b6af359ea61bc71e59efb4802ff01cce728c (diff)
Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12888 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions