aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml4
-rw-r--r--printing/prettyp.ml15
-rw-r--r--printing/printer.ml24
-rw-r--r--printing/printer.mli8
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/proof_diffs.ml14
-rw-r--r--printing/proof_diffs.mli6
7 files changed, 38 insertions, 37 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index e38da45b95..418e13759b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -295,7 +295,7 @@ let tag_var = tag Tag.variable
| CPatOr pl ->
hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
- | CPatNotation ("( _ )",([p],[]),[]) ->
+ | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
| CPatNotation (s,(l,ll),args) ->
@@ -665,7 +665,7 @@ let tag_var = tag Tag.variable
| CastCoerce -> str ":>"),
lcast
)
- | CNotation ("( _ )",([t],[],[],[])) ->
+ | CNotation ((_,"( _ )"),([t],[],[],[])) ->
return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
| CNotation (s,env) ->
pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd7135b6a6..1810cc6588 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -98,7 +98,8 @@ let print_ref reduce ref udecl =
(Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let inst =
- if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+ if Global.is_polymorphic ref
+ then Printer.pr_universe_instance sigma (Univ.UContext.instance univs)
else mt ()
in
hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
@@ -552,8 +553,7 @@ let print_instance sigma cb =
if Declareops.constant_is_polymorphic cb then
let univs = Declareops.constant_polymorphic_context cb in
let inst = Univ.AUContext.instance univs in
- let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
- pr_universe_instance sigma univs
+ pr_universe_instance sigma inst
else mt()
let print_constant with_values sep sp udecl =
@@ -657,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent =
gallina_print_leaf_entry env sigma with_values (oname,lobj)
| (oname,Lib.OpenedSection (dir,_)) ->
Some (str " >>>>>>> Section " ++ pr_name oname)
- | (oname,Lib.ClosedSection _) ->
- Some (str " >>>>>>> Closed Section " ++ pr_name oname)
| (_,Lib.CompilingLibrary { obj_dir; _ }) ->
Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
| (oname,Lib.OpenedModule _) ->
Some (str " >>>>>>> Module " ++ pr_name oname)
- | (oname,Lib.ClosedModule _) ->
- Some (str " >>>>>>> Closed Module " ++ pr_name oname)
let gallina_print_context env sigma with_values =
let rec prec n = function
@@ -793,9 +789,6 @@ let read_sec_context qid =
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
- | (_,Lib.ClosedSection _)::rest ->
- user_err Pp.(str "Cannot print the contents of a closed section.")
- (* LEM: Actually, we could if we wanted to. *)
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest
in
@@ -909,7 +902,7 @@ let inspect env sigma depth =
open Classops
-let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
+let print_coercion_value env sigma v = Printer.pr_global v.coe_value
let print_class i =
let cl,_ = class_info_from_index i in
diff --git a/printing/printer.ml b/printing/printer.ml
index ba094596ff..5b3ead181f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -82,11 +82,10 @@ let pr_econstr_n_core goal_concl_style env sigma n t =
pr_constr_expr_n n (extern_constr goal_concl_style env sigma t)
let pr_econstr_core goal_concl_style env sigma t =
pr_constr_expr (extern_constr goal_concl_style env sigma t)
-let pr_leconstr_core goal_concl_style env sigma t =
- pr_lconstr_expr (extern_constr goal_concl_style env sigma t)
+let pr_leconstr_core = Proof_diffs.pr_leconstr_core
let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
-let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+let pr_lconstr_env = Proof_diffs.pr_lconstr_env
let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
let _ = Hook.set Refine.pr_constr pr_constr_env
@@ -133,8 +132,7 @@ let pr_lconstr_under_binders c =
let pr_etype_core goal_concl_style env sigma t =
pr_constr_expr (extern_type goal_concl_style env sigma t)
-let pr_letype_core goal_concl_style env sigma t =
- pr_lconstr_expr (extern_type goal_concl_style env sigma t)
+let pr_letype_core = Proof_diffs.pr_letype_core
let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
@@ -290,11 +288,13 @@ let pr_cumulativity_info sigma cumi =
let pr_global_env = pr_global_env
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 UnivNames.pr_with_global_universes u ++ str"*)"
- else mt ())
+let pr_universe_instance evd inst =
+ str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+
+let pr_puniverses f env sigma (c,u) =
+ if !Constrextern.print_universes
+ then f env c ++ pr_universe_instance sigma u
+ else f env c
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
let pr_existential_key = Termops.pr_existential_key
@@ -1016,10 +1016,6 @@ let pr_polymorphic b =
if b then str"Polymorphic " else str"Monomorphic "
else mt ()
-let pr_universe_instance evd ctx =
- let inst = Univ.UContext.instance ctx in
- str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
-
(* print the proof step, possibly with diffs highlighted, *)
let print_and_diff oldp newp =
match newp with
diff --git a/printing/printer.mli b/printing/printer.mli
index 948b06f3f6..971241d5f9 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t
val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
-val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t
val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
@@ -139,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t
val pr_inductive : env -> inductive -> Pp.t
val pr_evaluable_reference : evaluable_global_reference -> Pp.t
-val pr_pconstant : env -> pconstant -> Pp.t
-val pr_pinductive : env -> pinductive -> Pp.t
-val pr_pconstructor : env -> pconstructor -> Pp.t
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
(** Contexts *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3f95dcfb6d..e2d9850bf8 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
- let ctx = Declareops.inductive_polymorphic_context mib in
- let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
- Printer.pr_universe_instance sigma ctx
+ Printer.pr_universe_instance sigma u
else mt ()
in
hov 0 (
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 7131ced15b..3a81e908a7 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -251,6 +251,11 @@ let pr_letype_core goal_concl_style env sigma t =
let pp_of_type env sigma ty =
pr_letype_core true env sigma EConstr.(of_constr ty)
+let pr_leconstr_core goal_concl_style env sigma t =
+ Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t)
+
+let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+
(* fetch info from a goal, returning (idents, map, concl_pp) where
idents is a list with one entry for each hypothesis, each entry is the list of
idents on the lhs of the hypothesis. map is a map from ident to hyp_info
@@ -278,10 +283,13 @@ let goal_info goal sigma =
line_idents := idents :: !line_idents;
let mid = match body with
- | Some x -> str " := " ++ pp_of_type env sigma ty ++ str " : "
- | None -> str " : " in
+ | Some c ->
+ let pb = pr_lconstr_env env sigma c in
+ let pb = if Constr.isCast c then surround pb else pb in
+ str " := " ++ pb
+ | None -> mt() in
let ts = pp_of_type env sigma ty in
- let rhs_pp = mid ++ ts in
+ let rhs_pp = mid ++ str " : " ++ ts in
let make_entry () = { idents; rhs_pp; done_ = false } in
List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 0d3b5821e5..482f03b686 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -30,6 +30,8 @@ val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t
open Evd
open Proof_type
+open Environ
+open Constr
(** Computes the diff between two goals
@@ -46,6 +48,10 @@ val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t
(** Convert a string to a list of token strings using the lexer *)
val tokenize_string : string -> string list
+val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
+val pr_lconstr_env : env -> evar_map -> constr -> Pp.t
+
(* Exposed for unit test, don't use these otherwise *)
(* output channel for the test log file *)
val log_out_ch : out_channel ref
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 11:01:38 +0000