From d0a324eef4d35a87e300a2b660b26fdbe2043d92 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 20 May 2005 15:54:50 +0000 Subject: Adoption du nom canonique global_of_constr pour éviter confusion avec type reference MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 3 ++- library/libnames.mli | 9 +++++---- 2 files changed, 7 insertions(+), 5 deletions(-) (limited to 'library') diff --git a/library/libnames.ml b/library/libnames.ml index 361c01696..b7ec0c223 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -34,7 +34,7 @@ let subst_global subst ref = match ref with if kn==kn' then ref, mkConstruct ((kn,i),j) else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j) -let reference_of_constr c = match kind_of_term c with +let global_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp | Ind ind_sp -> IndRef ind_sp | Construct cstr_cp -> ConstructRef cstr_cp @@ -48,6 +48,7 @@ let constr_of_global = function | IndRef sp -> mkInd sp let constr_of_reference = constr_of_global +let reference_of_constr = global_of_constr module RefOrdered = struct diff --git a/library/libnames.mli b/library/libnames.mli index 43e31d08f..a9051623f 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -28,11 +28,12 @@ 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 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 -- cgit v1.2.3