diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
commit | 6715e6801c1d285a12eeca55dd8b831d7efb8c0d (patch) | |
tree | 2b8925708d85f7cef5fb222d551cf809704f8ebd /printing/prettyp.ml | |
parent | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (diff) | |
parent | 133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce (diff) |
Merge PR #7797: Remove reference name type.
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r-- | printing/prettyp.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fe6cf73c7..5e5d00362 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -344,8 +344,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -452,8 +451,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -787,10 +785,9 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + try Nametab.locate_section qid with Not_found -> user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function |