aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml18
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/prettyp.ml11
-rw-r--r--printing/prettyp.mli20
-rw-r--r--printing/printer.ml6
5 files changed, 27 insertions, 30 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 605781993..e38da45b9 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -159,7 +159,7 @@ let tag_var = tag Tag.variable
let pr_univ_expr = function
| Some (x,n) ->
- pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+ pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
| None -> str"_"
let pr_univ l =
@@ -180,7 +180,7 @@ let tag_var = tag Tag.variable
| GSet -> tag_type (str "Set")
| GType UUnknown -> tag_type (str "Type")
| GType UAnonymous -> tag_type (str "_")
- | GType (UNamed u) -> tag_type (pr_reference u)
+ | GType (UNamed u) -> tag_type (pr_qualid u)
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
@@ -205,16 +205,16 @@ let tag_var = tag Tag.variable
tag_type (str "Set")
| GType u ->
(match u with
- | UNamed u -> pr_reference u
+ | UNamed u -> pr_qualid u
| UAnonymous -> tag_type (str "Type")
| UUnknown -> tag_type (str "_"))
let pr_universe_instance l =
pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
- let pr_reference = CAst.with_val (function
- | Qualid qid -> pr_qualid qid
- | Ident id -> tag_var (pr_id id))
+ let pr_reference qid =
+ if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
+ else pr_qualid qid
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
@@ -564,9 +564,9 @@ let tag_var = tag Tag.variable
return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
else
return (p, lproj)
- | CAppExpl ((None,{v=Ident var},us),[t])
- | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None])
- when Id.equal var Notation_ops.ldots_var ->
+ | CAppExpl ((None,qid,us),[t])
+ | CApp ((_, {v = CRef(qid,us)}),[t,None])
+ when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
return (
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
larg
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index ce37c3614..bca419c9a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) ->
lident option * recursion_order_expr ->
Pp.t
-val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
val pr_binders : local_binder_expr list -> Pp.t
val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
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
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 0375cfc92..8dd729610 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -24,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node
val print_full_context : env -> Evd.evar_map -> Pp.t
val print_full_context_typ : env -> Evd.evar_map -> Pp.t
val print_full_pure_context : env -> Evd.evar_map -> Pp.t
-val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t
-val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
val print_eval :
reduction_function -> env -> Evd.evar_map ->
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
-val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
UnivNames.univ_name_list option -> Pp.t
-val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
val print_graph : env -> evar_map -> Pp.t
@@ -77,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit
name describing the kind of objects considered and that is added as a
grammar command prefix for vernacular commands Locate. *)
-val print_located_qualid : reference -> Pp.t
-val print_located_term : reference -> Pp.t
-val print_located_module : reference -> Pp.t
-val print_located_other : string -> reference -> Pp.t
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
type object_pr = {
print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 72030dc9f..d76bd1e2b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -229,15 +229,15 @@ let dirpath_of_global = function
dirpath_of_mp (MutInd.modpath kn)
| VarRef _ -> DirPath.empty
-let qualid_of_global env r =
- Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+let qualid_of_global ?loc env r =
+ Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r)
let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref ?loc vars r =
try orig_extern_ref vars r
with e when CErrors.noncritical e ->
- CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
+ qualid_of_global ?loc env r
in
Constrextern.set_extern_reference extern_ref;
try
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:32:41 +0000