From 7d381fb8b9a297b5802a36d9781012db55a83c38 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 20:27:22 +0000 Subject: 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 --- kernel/mod_subst.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'kernel/mod_subst.ml') 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 -- cgit v1.2.3