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