aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml351
1 files changed, 171 insertions, 180 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 199aa79c63..94b514239a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -15,9 +15,7 @@ open Names
open Constr
open Environ
open Globnames
-open Nametab
open Evd
-open Proof_type
open Refiner
open Constrextern
open Ppconstr
@@ -82,37 +80,21 @@ 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
let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
-let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c
-let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c
-
let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
-(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
-let pr_lconstr t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_lconstr_env env sigma t
-let pr_constr t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_constr_env env sigma t
-
-let pr_open_lconstr (_,c) = pr_lconstr c
-let pr_open_constr (_,c) = pr_constr c
-
-let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c)
-let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
+let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c
let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
(* Warning: clashes can occur with variables of same name in env but *)
@@ -124,28 +106,13 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
-let pr_constr_under_binders c =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_constr_under_binders_env env sigma c
-let pr_lconstr_under_binders c =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_lconstr_under_binders_env env sigma 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)
-let pr_ltype t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_ltype_env env sigma t
-let pr_type t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_type_env env sigma t
-
let pr_etype_env env sigma c = pr_etype_core false env sigma c
let pr_letype_env env sigma c = pr_letype_core false env sigma c
let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
@@ -153,29 +120,15 @@ let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
let pr_ljudge_env env sigma j =
(pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
-let pr_ljudge j =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_ljudge_env env sigma j
-
let pr_lglob_constr_env env c =
pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
let pr_glob_constr_env env c =
pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
-let pr_lglob_constr c =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_lglob_constr_env env c
-let pr_glob_constr c =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_glob_constr_env env c
-
let pr_closed_glob_n_env env sigma n c =
pr_constr_expr_n n (extern_closed_glob false env sigma c)
let pr_closed_glob_env env sigma c =
pr_constr_expr (extern_closed_glob false env sigma c)
-let pr_closed_glob c =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_closed_glob_env env sigma c
let pr_lconstr_pattern_env env sigma c =
pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
@@ -185,19 +138,12 @@ let pr_constr_pattern_env env sigma c =
let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
-let pr_lconstr_pattern t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_lconstr_pattern_env env sigma t
-let pr_constr_pattern t =
- let (sigma, env) = Pfedit.get_current_context () in
- pr_constr_pattern_env env sigma t
-
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
-let _ = Termops.set_print_constr
+let _ = Termops.Internal.set_print_constr
(fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
-let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
+let pr_in_comment x = str "(* " ++ x ++ str " *)"
(** Term printers resilient to [Nametab] errors *)
@@ -229,15 +175,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
@@ -250,57 +196,79 @@ let safe_gen f env sigma c =
let safe_pr_lconstr_env = safe_gen pr_lconstr_env
let safe_pr_constr_env = safe_gen pr_constr_env
-let safe_pr_lconstr t =
- let (sigma, env) = Pfedit.get_current_context () in
- safe_pr_lconstr_env env sigma t
-
-let safe_pr_constr t =
- let (sigma, env) = Pfedit.get_current_context () in
- safe_pr_constr_env env sigma t
let pr_universe_ctx_set sigma c =
if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
- fnl()++pr_in_comment (fun c -> v 0
- (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+ fnl()++pr_in_comment (v 0 (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c))
else
mt()
let pr_universe_ctx sigma ?variance c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
- fnl()++pr_in_comment (fun c -> v 0
- (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
+ fnl()++pr_in_comment (v 0 (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c))
else
mt()
-let pr_constant_universes sigma = function
- | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
- | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+let pr_abstract_universe_ctx sigma ?variance c ~priv =
+ let open Univ in
+ let priv = Option.default Univ.ContextSet.empty priv in
+ let has_priv = not (ContextSet.is_empty priv) in
+ if !Detyping.print_universes && (not (Univ.AUContext.is_empty c) || has_priv) then
+ let prlev u = Termops.pr_evd_level sigma u in
+ let pub = (if has_priv then str "Public universes:" ++ fnl() else mt()) ++ v 0 (Univ.pr_abstract_universe_context prlev ?variance c) in
+ let priv = if has_priv then fnl() ++ str "Private universes:" ++ fnl() ++ v 0 (Univ.pr_universe_context_set prlev priv) else mt() in
+ fnl()++pr_in_comment (pub ++ priv)
+ else
+ mt()
+
+let pr_constant_universes sigma ~priv = function
+ | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
+ | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx ~priv
let pr_cumulativity_info sigma cumi =
if !Detyping.print_universes
&& not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
- fnl()++pr_in_comment (fun uii -> v 0
- (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+ fnl()++pr_in_comment (v 0 (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) cumi))
+ else
+ mt()
+
+let pr_abstract_cumulativity_info sigma cumi =
+ if !Detyping.print_universes
+ && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
+ fnl()++pr_in_comment (v 0 (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) cumi))
else
mt()
(**********************************************************************)
(* Global references *)
-let pr_global_env = pr_global_env
+let pr_global_env = Nametab.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 Universes.pr_with_global_universes u ++ str"*)"
- else mt ())
+let pr_universe_instance_constraints evd inst csts =
+ let open Univ in
+ let prlev = Termops.pr_evd_level evd in
+ let pcsts = if Constraint.is_empty csts then mt()
+ else str " |= " ++
+ prlist_with_sep (fun () -> str "," ++ spc())
+ (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v))
+ (Constraint.elements csts)
+ in
+ str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}"
+
+let pr_universe_instance evd inst =
+ pr_universe_instance_constraints evd inst Univ.Constraint.empty
+
+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
let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
-let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
-let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
+let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr)
let pr_pconstant = pr_puniverses pr_constant
let pr_pinductive = pr_puniverses pr_inductive
@@ -489,20 +457,27 @@ let pr_predicate pr_elt (b, elts) =
let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
-let pr_transparent_state (ids, csts) =
- hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
- str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
-
-(* display complete goal *)
-let default_pr_goal gs =
- let g = sig_it gs in
- let sigma = project gs in
+let pr_transparent_state ts =
+ hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++
+ str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ())
+
+(* display complete goal
+ og_s has goal+sigma on the previous proof step for diffs
+ g_s has goal+sigma on the current proof step
+ *)
+let pr_goal ?(diffs=false) ?og_s g_s =
+ let g = sig_it g_s in
+ let sigma = project g_s in
let env = Goal.V82.env sigma g in
let concl = Goal.V82.concl sigma g in
let goal =
- pr_context_of env sigma ++ cut () ++
- str "============================" ++ cut () ++
- pr_goal_concl_style_env env sigma concl in
+ if diffs then
+ Proof_diffs.diff_goal ?og_s g sigma
+ else
+ pr_context_of env sigma ++ cut () ++
+ str "============================" ++ cut () ++
+ pr_goal_concl_style_env env sigma concl
+ in
str " " ++ v 0 goal
(* display a goal tag *)
@@ -518,13 +493,18 @@ let pr_goal_name sigma g =
let pr_goal_header nme sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
- ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
+ ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
(* display the conclusion of a goal *)
-let pr_concl n sigma g =
+let pr_concl n ?(diffs=false) ?og_s sigma g =
let (g,sigma) = Goal.V82.nf_evar sigma g in
let env = Goal.V82.env sigma g in
- let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+ let pc =
+ if diffs then
+ Proof_diffs.diff_concl ?og_s sigma g
+ else
+ pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+ in
let header = pr_goal_header (int n) sigma g in
header ++ str " is:" ++ cut () ++ str" " ++ pc
@@ -541,12 +521,12 @@ let pr_evgl_sign sigma evi =
if List.is_empty ids then mt () else
(str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
- let pc = pr_lconstr_env env sigma evi.evar_concl in
+ let pc = pr_leconstr_env env sigma evi.evar_concl in
let candidates =
match evi.evar_body, evi.evar_candidates with
| Evar_empty, Some l ->
spc () ++ str "= {" ++
- prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}"
+ prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}"
| _ ->
mt ()
in
@@ -591,11 +571,11 @@ let pr_ne_evar_set hd tl sigma l =
mt ()
let pr_selected_subgoal name sigma g =
- let pg = default_pr_goal { sigma=sigma ; it=g; } in
+ let pg = pr_goal { sigma=sigma ; it=g; } in
let header = pr_goal_header name sigma g in
v 0 (header ++ str " is:" ++ cut () ++ pg)
-let default_pr_subgoal n sigma =
+let pr_subgoal n sigma =
let rec prrec p = function
| [] -> user_err Pp.(str "No such goal.")
| g::rest ->
@@ -622,8 +602,8 @@ let print_evar_constraints gl sigma =
end
in
let pr_evconstr (pbty,env,t1,t2) =
- let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1)
- and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in
+ let t1 = Evarutil.nf_evar sigma t1
+ and t2 = Evarutil.nf_evar sigma t2 in
let env =
(** We currently allow evar instances to refer to anonymous de Bruijn
indices, so we protect the error printing code in this case by giving
@@ -691,12 +671,21 @@ let print_dependent_evars gl sigma seeds =
in
constraints ++ evars ()
+module GoalMap = Evar.Map
+
(* Print open subgoals. Checks for uninstantiated existential variables *)
(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
(* spiwack: [pr_first] is true when the first goal must be singled out
and printed in its entirety. *)
-let default_pr_subgoals ?(pr_first=true)
+(* [os_map] is derived from the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
+ let diff_goal_map =
+ match os_map with
+ | Some (_, diff_goal_map) -> diff_goal_map
+ | None -> GoalMap.empty
+ in
+
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
@@ -729,17 +718,29 @@ let default_pr_subgoals ?(pr_first=true)
if needed then str" focused "
else str" " (* non-breakable space *)
in
- (** Main function *)
+
+ let get_ogs g =
+ match os_map with
+ | Some (osigma, _) ->
+ (* if Not_found, returning None treats the goal as new and it will be highlighted;
+ returning Some { it = g; sigma = sigma } will compare the new goal
+ to itself and it won't be highlighted *)
+ (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma }
+ with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)"))
+ | None -> None
+ in
let rec pr_rec n = function
| [] -> (mt ())
| g::rest ->
- let pc = pr_concl n sigma g in
+ let og_s = get_ogs g in
+ let pc = pr_concl n ~diffs ?og_s sigma g in
let prest = pr_rec (n+1) rest in
(cut () ++ pc ++ prest)
in
let print_multiple_goals g l =
if pr_first then
- default_pr_goal { it = g ; sigma = sigma; }
+ let og_s = get_ogs g in
+ pr_goal ~diffs ?og_s { it = g ; sigma = sigma }
++ (if l=[] then mt () else cut ())
++ pr_rec 2 l
else
@@ -751,6 +752,8 @@ let default_pr_subgoals ?(pr_first=true)
| Some cmd -> Feedback.msg_info cmd
| None -> ()
in
+
+ (** Main function *)
match goals with
| [] ->
begin
@@ -780,34 +783,7 @@ let default_pr_subgoals ?(pr_first=true)
++ print_dependent_evars (Some g1) sigma seeds
)
-(**********************************************************************)
-(* Abstraction layer *)
-
-
-type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
- pr_subgoal : int -> evar_map -> goal list -> Pp.t;
- pr_goal : goal sigma -> Pp.t;
-}
-
-let default_printer_pr = {
- pr_subgoals = default_pr_subgoals;
- pr_subgoal = default_pr_subgoal;
- pr_goal = default_pr_goal;
-}
-
-let printer_pr = ref default_printer_pr
-
-let set_printer_pr = (:=) printer_pr
-
-let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
-let pr_subgoal x = !printer_pr.pr_subgoal x
-let pr_goal x = !printer_pr.pr_goal x
-
-(* End abstraction layer *)
-(**********************************************************************)
-
-let pr_open_subgoals ~proof =
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
(* spiwack: it shouldn't be the job of the printer to look up stuff
in the [evar_map], I did stuff that way because it was more
straightforward, but seriously, [Proof.proof] should return
@@ -830,21 +806,33 @@ let pr_open_subgoals ~proof =
fnl ()
++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf
| _ , _, _ ->
- let end_cmd =
- str "This subproof is complete, but there are some unfocused goals." ++
- (let s = Proof_bullet.suggest p in
- if Pp.ismt s then s else fnl () ++ s) ++
- fnl ()
+ let cmd = if quiet then None else
+ Some
+ (str "This subproof is complete, but there are some unfocused goals." ++
+ (let s = Proof_bullet.suggest p in
+ if Pp.ismt s then s else fnl () ++ s) ++
+ fnl ())
in
- pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
+ pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
end
| _ ->
let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
- pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
+ let os_map = match oproof with
+ | Some op when diffs ->
+ let (_,_,_,_, osigma) = Proof.proof op in
+ let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
+ Some (osigma, diff_goal_map)
+ | _ -> None
+ in
+ pr_subgoals ~pr_first:true ~diffs ?os_map None bsigma ~seeds ~shelf ~stack:[]
+ ~unfocused:unfocused_if_needed ~goals:bgoals_focused
end
+let pr_open_subgoals ~proof =
+ pr_open_subgoals_diff proof
+
let pr_nth_open_subgoal ~proof n =
let gls,_,_,_,sigma = Proof.proof proof in
pr_subgoal n sigma gls
@@ -856,19 +844,6 @@ let pr_goal_by_id ~proof id =
pr_selected_subgoal (pr_id id) sigma g)
with Not_found -> user_err Pp.(str "No such goal.")
-(* Elementary tactics *)
-
-let pr_prim_rule = function
- | Refine c ->
- (** FIXME *)
- str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++
- Constrextern.with_meta_as_hole pr_constr c
-
-(* Backwards compatibility *)
-
-let prterm = pr_lconstr
-
-
(* Printer function for sets of Assumptions.assumptions.
It is used primarily by the Print Assumptions command. *)
@@ -879,7 +854,7 @@ type axiom =
type context_object =
| Variable of Id.t (* A section variable or a Let definition *)
- | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+ | Axiom of axiom * (Label.t * Constr.rel_context * types) list
| Opaque of Constant.t (* An opaque constant. *)
| Transparent of Constant.t
@@ -925,11 +900,18 @@ let pr_assumptionset env sigma s =
let safe_pr_constant env kn =
try pr_constant env kn
with Not_found ->
- let mp,_,lab = Constant.repr3 kn in
+ (* FIXME? *)
+ let mp,lab = Constant.repr2 kn in
str (ModPath.to_string mp) ++ str "." ++ Label.print lab
in
- let safe_pr_ltype typ =
- try str " : " ++ pr_ltype typ
+ let safe_pr_inductive env kn =
+ try pr_inductive env (kn,0)
+ with Not_found ->
+ (* FIXME? *)
+ MutInd.print kn
+ in
+ let safe_pr_ltype env sigma typ =
+ try str " : " ++ pr_ltype_env env sigma typ
with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
@@ -940,9 +922,9 @@ let pr_assumptionset env sigma s =
let pr_axiom env ax typ =
match ax with
| Constant kn ->
- safe_pr_constant env kn ++ safe_pr_ltype typ
+ safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
| Positive m ->
- hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.")
+ hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
| Guarded kn ->
hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
in
@@ -950,7 +932,7 @@ let pr_assumptionset env sigma s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = pr_id id ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in
(var :: v, a, o, tr)
| Axiom (axiom, []) ->
let ax = pr_axiom env axiom typ in
@@ -964,10 +946,10 @@ let pr_assumptionset env sigma s =
l in
(v, ax :: a, o, tr)
| Opaque kn ->
- let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let opq = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, opq :: o, tr)
| Transparent kn ->
- let tran = safe_pr_constant env kn ++ safe_pr_ltype typ in
+ let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in
(v, a, o, tran :: tr)
in
let (vars, axioms, opaque, trans) =
@@ -1000,20 +982,29 @@ let pr_assumptionset env sigma s =
] in
prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
-let xor a b =
- (a && not b) || (not a && b)
-
let pr_cumulative poly cum =
if poly then
if cum then str "Cumulative " else str "NonCumulative "
else mt ()
let pr_polymorphic b =
- let print = xor (Flags.is_universe_polymorphism ()) b in
- if print then
- 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"}"
+ if b then str"Polymorphic " else str"Monomorphic "
+
+(* print the proof step, possibly with diffs highlighted, *)
+let print_and_diff oldp newp =
+ match newp with
+ | None -> ()
+ | Some proof ->
+ let output =
+ if Proof_diffs.show_diffs () then
+ try pr_open_subgoals_diff ~diffs:true ?oproof:oldp proof
+ with Pp_diff.Diff_Failure msg -> begin
+ (* todo: print the unparsable string (if we know it) *)
+ Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+ ++ str "Showing results without diff highlighting" );
+ pr_open_subgoals ~proof
+ end
+ else
+ pr_open_subgoals ~proof
+ in
+ Feedback.msg_notice output;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:33:29 +0000