aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorherbelin2003-08-31 19:55:48 +0000
committerherbelin2003-08-31 19:55:48 +0000
commitb0579cf0d372f8d79f6f776149c7dc3f59f29181 (patch)
tree163bcc136797388f49c571beeff32f69b30b07d8 /dev/include
parentdbada45eec1e3fab8e14e99660a565ee87b3700a (diff)
Symetrisation des changements implicites de scope
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions