aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:22 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:22 +0000
commit7d381fb8b9a297b5802a36d9781012db55a83c38 (patch)
treec2f2199651a99275c2d07ec59cb4da0da2ba6fe8 /library/nametab.ml
parent81b527990c64a03a8b6942a7a0477e35ed144a76 (diff)
Mod_subst: an extra assert
It seems that the Equiv delta_hint in a resolver have a particular shape: a kn can apparently only be shifted to another kn with same label this way. We validate this fact via an assert, since this isn't obvious (due to recursive calls in Mod_subst and Modops), and since this implies the important fact that user and canonical parts of kernel pairs have necessarily the same label (and section dirpath). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16219 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
0 files changed, 0 insertions, 0 deletions