aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorherbelin2003-10-14 10:49:27 +0000
committerherbelin2003-10-14 10:49:27 +0000
commit81eae968edff0dde3fba1a72717813fbca1bccb3 (patch)
tree3869a1f7175794158dad45c4ebfd2df96d486662 /dev/include
parent7a533b316f965fb8391511638858a4dfa4a112a1 (diff)
identityT = identity
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions