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
---
 kernel/safe_typing.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e5b8412ec0..3c4c50a4ae 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -475,18 +475,10 @@ let end_module l restype senv =
      let new_name = match elem with
        | SFBconst _ ->
 	   let kn = make_kn mp_sup empty_dirpath l in
-	   let con = constant_of_kn_equiv kn
-	     (canonical_con
-		(constant_of_delta resolver (constant_of_kn kn)))
-	   in
-	   C con
+	   C (constant_of_delta_kn resolver kn)
        | SFBmind _ ->
 	   let kn = make_kn mp_sup empty_dirpath l in
-	   let mind = mind_of_kn_equiv kn
-	     (canonical_mind
-		(mind_of_delta resolver (mind_of_kn kn)))
-	   in
-	   I mind
+	   I (mind_of_delta_kn resolver kn)
        | SFBmodule _ -> M
        | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l))
      in
-- 
cgit v1.2.3