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/mod_subst.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index bf08841c83..275c6e6775 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -147,6 +147,9 @@ let gen_of_delta resolve x kn fix_can =
     if kn == new_kn then x else fix_can new_kn
   with _ -> x
 
+let constant_of_delta_kn resolve kn =
+  gen_of_delta resolve (constant_of_kn kn) kn (constant_of_kn_equiv kn)
+
 let constant_of_delta resolve con =
   let kn = user_con con in
   gen_of_delta resolve con kn (constant_of_kn_equiv kn)
@@ -155,6 +158,9 @@ let constant_of_delta2 resolve con =
   let kn, kn' = canonical_con con, user_con con in
   gen_of_delta resolve con kn (constant_of_kn_equiv kn')
 
+let mind_of_delta_kn resolve kn =
+  gen_of_delta resolve (mind_of_kn kn) kn (mind_of_kn_equiv kn)
+
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
   gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
-- 
cgit v1.2.3