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

1 files changed, 7 insertions, 2 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 817716c2d..303c65c38 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -19,7 +19,7 @@ open Names
 open Term
 
 (* For Inline, the int is an inlining level, and the constr (if present)
-   is the term into which we should inline *)
+   is the term into which we should inline. *)
 
 type delta_hint =
   | Inline of int * constr option
@@ -45,6 +45,9 @@ module Deltamap = struct
   let join map1 map2 = fold add_mp add_kn map1 map2
 end
 
+(* Invariant: in the [delta_hint] map, an [Equiv] should only
+   relate [kernel_name] with the same label (and section dirpath). *)
+
 type delta_resolver = Deltamap.t
 
 let empty_delta_resolver = Deltamap.empty
@@ -120,7 +123,9 @@ let debug_pr_subst sub =
 
 let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc))
 
-let add_kn_delta_resolver kn kn' = Deltamap.add_kn kn (Equiv kn')
+let add_kn_delta_resolver kn kn' =
+  assert (Label.equal (label kn) (label kn'));
+  Deltamap.add_kn kn (Equiv kn')
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2