aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorherbelin2010-03-30 15:09:10 +0000
committerherbelin2010-03-30 15:09:10 +0000
commitc0e397fca7fd2f150c68ab043fd8fdd15db5bcdf (patch)
treedaf05944aefa6640ece4eefe04283aa93320ea96 /doc
parentf986fba6cfdbf923884da5fba4443964b0e725d5 (diff)
Fixed small bugs introduced in commit 12890 (bug #2286, that comes
from a incorrect computation of logical names + bug in rendering of name-based notations, aka abbreviations or syntactic definitions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions