diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 424cf1f73..d951b616e 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -264,3 +264,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" |