From 8c417a6d32e379d9642d6f2ef144f33d7df4832e Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Feb 2005 22:15:17 +0000 Subject: 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 --- library/libnames.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/libnames.mli') 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 -- cgit v1.2.3