From 0a94199867a80d5c9ee6aa52668b1c3b1dbb2cfa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Nov 2004 15:24:39 +0000
Subject: code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6288 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/libnames.ml  | 10 ----------
 library/libnames.mli |  3 ---
 2 files changed, 13 deletions(-)

diff --git a/library/libnames.ml b/library/libnames.ml
index 171e2b3b54..17fd50b7f2 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -188,16 +188,6 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of kernel_name
 
-let subst_ext subst glref = match glref with
-  | TrueGlobal ref -> 
-      let ref' = subst_global subst ref in
-	if ref' == ref then glref else
-	  TrueGlobal ref'
-  | SyntacticDef kn ->
-      let kn' = subst_kn subst kn in
-	if kn' == kn then glref else
-	  SyntacticDef kn'
-
 let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 
 let decode_kn kn = 
diff --git a/library/libnames.mli b/library/libnames.mli
index b00d51dc50..ffb51ec0bb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -82,9 +82,6 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of kernel_name
 
-val subst_ext : 
-  substitution -> extended_global_reference -> extended_global_reference
-
 (*s Temporary function to brutally form kernel names from section paths *)
 
 val encode_kn : dir_path -> identifier -> kernel_name
-- 
cgit v1.2.3