From e79b800bec660dc2724fa70c33f4e435ddbf885c Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 11 Oct 2011 09:06:05 +0000 Subject: Various simplifications about constant_of_delta and mind_of_delta Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/global.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'library/global.ml') diff --git a/library/global.ml b/library/global.ml index 6548e6537..ab70bb7c3 100644 --- a/library/global.ml +++ b/library/global.ml @@ -119,15 +119,19 @@ let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) let lookup_modtype kn = lookup_modtype kn (env()) -let constant_of_delta con = +let constant_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO : are resolver and resolver_param orthogonal ? + the effect of resolver is lost if resolver_param isn't + trivial at that spot. *) Mod_subst.constant_of_delta resolver_param - (Mod_subst.constant_of_delta resolver con) + (Mod_subst.constant_of_delta_kn resolver kn) -let mind_of_delta mind = +let mind_of_delta_kn kn = let resolver,resolver_param = (delta_of_senv !global_env) in + (* TODO idem *) Mod_subst.mind_of_delta resolver_param - (Mod_subst.mind_of_delta resolver mind) + (Mod_subst.mind_of_delta_kn resolver kn) let exists_label id = exists_label id !global_env -- cgit v1.2.3