diff options
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 |