diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:15:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 22:15:17 +0000 |
| commit | 8c417a6d32e379d9642d6f2ef144f33d7df4832e (patch) | |
| tree | c5cb1faa4cfc2c7859f95e79c373fc11b687b79e /library/libnames.mli | |
| parent | 6c6d36a2169610dc80afb0023d7546e8ea4bd1c8 (diff) | |
Standardisation of constr_of_reference into constr_of_global + Moved Indmap and ConstrMap to Names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 8d4ba269d..43e31d08f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -26,6 +26,9 @@ type global_reference = val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) +val constr_of_global : global_reference -> constr + +(* Obsolete synonym for constr_of_global *) val constr_of_reference : global_reference -> constr (* Turn a construction denoting a global into a reference; @@ -35,9 +38,6 @@ 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 |