diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 18:07:16 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 18:07:16 +0000 |
commit | 43856804207ac43b9ded2609fe7a422db5f62dc4 (patch) | |
tree | e517f68ce2c43b719f7480ff8f45a0eec0298d46 /dev/tools/Makefile.devel | |
parent | 58c70113a815a42593c566f64f2de840fc7e48a1 (diff) |
one more substitution s/Set/Type/
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools/Makefile.devel')
0 files changed, 0 insertions, 0 deletions