diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /library/libnames.ml | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 48a7565e..07c9ad23 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*) +(*i $Id: libnames.ml 9488 2007-01-17 11:11:58Z herbelin $ i*) open Pp open Util @@ -21,6 +21,8 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor +let isVarRef = function VarRef _ -> true | _ -> false + let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> @@ -264,3 +266,18 @@ let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc +(* popping one level of section in global names *) + +let pop_con con = + let (mp,dir,l) = repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +let pop_kn kn = + let (mp,dir,l) = repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_global_reference = function + | ConstRef con -> ConstRef (pop_con con) + | IndRef (kn,i) -> IndRef (pop_kn kn,i) + | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) + | VarRef id -> anomaly "VarRef not poppable" |