From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 library/libnames.mli | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'library/libnames.mli')

diff --git a/library/libnames.mli b/library/libnames.mli
index a6055428..06595e81 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli,v 1.8.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: libnames.mli 7052 2005-05-20 15:54:50Z herbelin $ i*)
 
 (*i*)
 open Pp
 open Util
 open Names
 open Term
+open Mod_subst
 (*i*)
 
 (*s Global reference is a kernel side type for all references together *)
@@ -22,21 +23,22 @@ type global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
-val subst_global : substitution -> global_reference -> global_reference
+val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)
-val constr_of_reference : global_reference -> constr
+val constr_of_global : global_reference -> constr
+
+(* Turn a construction denoting a global reference into a global reference;
+   raise [Not_found] if not a global reference *)
+val global_of_constr : constr -> global_reference
 
-(* Turn a construction denoting a global into a reference;
-   raise [Not_found] if not a global *)
+(* Obsolete synonyms for constr_of_global and global_of_constr *)
+val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
 module Refset : Set.S with type elt = global_reference 
 module Refmap : Map.S with type key = global_reference
 
-module Indmap : Map.S with type key = inductive
-module Constrmap : Map.S with type key = constructor
-
 (*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
@@ -82,13 +84,12 @@ 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
 val decode_kn : kernel_name -> dir_path * identifier
+val encode_con : dir_path -> identifier -> constant
+val decode_con : constant -> dir_path * identifier
 
 
 (*s A [qualid] is a partially qualified ident; it includes fully
-- 
cgit v1.2.3