summaryrefslogtreecommitdiff
path: root/library/libnames.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /library/libnames.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'library/libnames.mli')
-rw-r--r--library/libnames.mli23
1 files changed, 12 insertions, 11 deletions
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