From 7d37a17370cfdfcc13afde93f5943ae53ea4d599 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 7 Dec 2004 19:48:17 +0000
Subject: * added subst_evaluable_reference * the Unfold hints of auto/eauto
 now use evaluable_global_references in place   of global_references

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6428 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_subst.ml  | 4 ++++
 kernel/mod_subst.mli | 3 +++
 2 files changed, 7 insertions(+)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ba186d06e9..48bb9933ce 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -123,6 +123,10 @@ let subst_con sub con =
   let mp' = subst_mp sub mp in
     if mp==mp' then con else make_con mp' dir l
 
+let subst_evaluable_reference subst = function
+  | EvalVarRef id -> EvalVarRef id
+  | EvalConstRef kn -> EvalConstRef (subst_con subst kn)
+
 (* 
 map_kn : (kernel_name -> kernel_name) -> constr -> constr
 
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fa37c25092..f4003c7f95 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -55,6 +55,9 @@ val occur_mbid : mod_bound_id -> substitution -> bool
 
 val subst_kn : substitution -> kernel_name -> kernel_name
 val subst_con : substitution -> constant -> constant
+val subst_evaluable_reference :
+  substitution -> evaluable_global_reference -> evaluable_global_reference
+
 
 (* [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)
-- 
cgit v1.2.3