diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /library/libnames.mli | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 23 |
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 |