aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml6
-rw-r--r--printing/ppconstr.mli4
-rw-r--r--printing/ppvernac.ml21
-rw-r--r--printing/prettyp.ml11
-rw-r--r--printing/prettyp.mli11
-rw-r--r--printing/printer.ml2
-rw-r--r--printing/printer.mli5
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/printmod.mli2
9 files changed, 33 insertions, 33 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 412a1cbb41..60268c9de6 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -170,13 +170,13 @@ let tag_var = tag Tag.variable
let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
- let pr_glob_sort = function
+ let pr_glob_sort = let open Glob_term in function
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType [] -> tag_type (str "Type")
| GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
- let pr_glob_level = function
+ let pr_glob_level = let open Glob_term in function
| GProp -> tag_type (str "Prop")
| GSet -> tag_type (str "Set")
| GType UUnknown -> tag_type (str "Type")
@@ -199,7 +199,7 @@ let tag_var = tag Tag.variable
let pr_qualid = pr_qualid
let pr_patvar = pr_id
- let pr_glob_sort_instance = function
+ let pr_glob_sort_instance = let open Glob_term in function
| GProp ->
tag_type (str "Prop")
| GSet ->
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1f1308b0df..127c4471cd 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -41,8 +41,8 @@ val pr_name : Name.t -> Pp.t
val pr_qualid : qualid -> Pp.t
val pr_patvar : patvar -> Pp.t
-val pr_glob_level : glob_level -> Pp.t
-val pr_glob_sort : glob_sort -> Pp.t
+val pr_glob_level : Glob_term.glob_level -> Pp.t
+val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_guard_annot : (constr_expr -> Pp.t) ->
local_binder_expr list ->
lident option * recursion_order_expr ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7eb8396ac8..7a34e80274 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -16,12 +16,13 @@ open Util
open CAst
open Extend
-open Vernacexpr
-open Pputils
open Libnames
+open Decl_kinds
open Constrexpr
open Constrexpr_ops
-open Decl_kinds
+open Vernacexpr
+open Declaremods
+open Pputils
open Ppconstr
@@ -144,7 +145,7 @@ open Decl_kinds
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
| SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -187,7 +188,7 @@ open Decl_kinds
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
- let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+ let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
pr_opt (fun x -> str"|" ++ int x) pri ++
pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
@@ -507,7 +508,7 @@ open Decl_kinds
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
| PrintAbout (qid,l,gopt) ->
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
@@ -716,6 +717,7 @@ open Decl_kinds
return (keyword "Admitted")
| VernacEndProof (Proved (opac,o)) -> return (
+ let open Proof_global in
match o with
| None -> (match opac with
| Transparent -> keyword "Defined"
@@ -1121,7 +1123,7 @@ open Decl_kinds
| None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
in
let pr_i = match io with None -> mt ()
- | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
+ | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
return (pr_i ++ pr_mayeval r c)
| VernacGlobalCheck c ->
return (hov 2 (keyword "Type" ++ pr_constrarg c))
@@ -1175,7 +1177,8 @@ open Decl_kinds
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
| VernacBullet b ->
- return (begin match b with
+ (* XXX: Redundant with Proof_bullet.print *)
+ return (let open Proof_bullet in begin match b with
| Dash n -> str (String.make n '-')
| Star n -> str (String.make n '*')
| Plus n -> str (String.make n '+')
@@ -1183,7 +1186,7 @@ open Decl_kinds
| VernacSubproof None ->
return (str "{")
| VernacSubproof (Some i) ->
- return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+ return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
| VernacEndSubproof ->
return (str "}")
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f17d844f7..d036fec21a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,8 +35,8 @@ open Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
@@ -93,7 +93,7 @@ let print_ref reduce ref udecl =
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
- let bl = Universes.universe_binders_with_opt_names ref
+ let bl = UnivNames.universe_binders_with_opt_names ref
(Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let inst =
@@ -328,7 +328,7 @@ type 'a locatable_info = {
type locatable = Locatable : 'a locatable_info -> locatable
type logical_name =
- | Term of global_reference
+ | Term of GlobRef.t
| Dir of global_dir_reference
| Syntactic of KerName.t
| ModuleType of ModPath.t
@@ -376,7 +376,6 @@ let pr_located_qualid = function
| DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir
| DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir
| DirModule { obj_dir ; _ } -> "Module", obj_dir
- | DirClosedSection dir -> "Closed Section", dir
in
str s ++ spc () ++ DirPath.print dir
| ModuleType mp ->
@@ -595,7 +594,7 @@ let print_constant with_values sep sp udecl =
in
let ctx =
UState.of_binders
- (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+ (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 213f0aeeb6..50042d6c5b 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,7 +12,6 @@ open Names
open Environ
open Reductionops
open Libnames
-open Globnames
open Misctypes
open Evd
@@ -35,10 +34,10 @@ val print_eval :
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
val print_name : env -> Evd.evar_map -> reference or_by_notation ->
- Universes.univ_name_list option -> Pp.t
+ 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 or_by_notation ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_impargs : reference or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
@@ -50,7 +49,7 @@ val print_canonical_projections : env -> Evd.evar_map -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
-val print_instances : global_reference -> Pp.t
+val print_instances : GlobRef.t -> Pp.t
val print_all_instances : unit -> Pp.t
val inspect : env -> Evd.evar_map -> int -> Pp.t
@@ -85,8 +84,8 @@ val print_located_module : reference -> Pp.t
val print_located_other : string -> reference -> Pp.t
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index edcce874d8..77466605a2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_global = pr_global_env Id.Set.empty
let pr_puniverses f env (c,u) =
f env c ++
(if !Constrextern.print_universes then
- str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
else mt ())
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
diff --git a/printing/printer.mli b/printing/printer.mli
index 41843680bc..4af90e6a62 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Globnames
open Constr
open Environ
open Pattern
@@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
(** Printing global references using names as short as possible *)
-val pr_global_env : Id.Set.t -> global_reference -> Pp.t
-val pr_global : global_reference -> Pp.t
+val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
+val pr_global : GlobRef.t -> Pp.t
val pr_constant : env -> Constant.t -> Pp.t
val pr_existential_key : evar_map -> Evar.t -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f3b..3c805b327d 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -140,7 +140,7 @@ let print_mutual_inductive env mind mib udecl =
(AUContext.instance (Declareops.inductive_polymorphic_context mib)))
else []
in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
Printer.pr_cumulative
@@ -183,7 +183,7 @@ let print_record env mind mib udecl =
let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
(Array.to_list (Univ.Instance.to_array u)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let keyword =
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0b0b0a35e..48ba866cc0 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool
val pr_mutual_inductive_body : Environ.env ->
MutInd.t -> Declarations.mutual_inductive_body ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_module : bool -> ModPath.t -> Pp.t
val print_modtype : ModPath.t -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:04:12 +0000